[thread-safety] propagate conditional writes to callers

Summary:
In code like
```
foo(o) {
  iWriteToF(o)
}
```
, the condtional write to `f` in `iWriteToF` should become a conditional write for `foo`.

Reviewed By: peterogithub

Differential Revision: D4429160

fbshipit-source-id: f111ac4

infer/src/checkers/ThreadSafety.ml

@@ -198,9 +198,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                                          safe *)
                                       acc
                                     else
-                                      cond_writes,
-                                      ThreadSafetyDomain.PathDomain.join
-                                        uncond_writes callee_cond_writes_for_index'
+                                      let base = fst actual_access_path in
+                                      begin
+                                        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 *)
+                                            let conditional_writes' =
+                                              try
+                                                ThreadSafetyDomain.ConditionalWritesDomain.find
+                                                  formal_index
+                                                  cond_writes
+                                                |> ThreadSafetyDomain.PathDomain.join
+                                                  callee_cond_writes_for_index'
+                                              with Not_found ->
+                                                callee_cond_writes_for_index' in
+                                            let cond_writes' =
+                                              ThreadSafetyDomain.ConditionalWritesDomain.add
+                                                formal_index conditional_writes' cond_writes in
+                                            cond_writes', uncond_writes
+                                        | None ->
+                                            (* access path not owned and not rooted in a formal. add
+                                               to unconditional writes *)
+                                            cond_writes,
+                                            ThreadSafetyDomain.PathDomain.join
+                                              uncond_writes callee_cond_writes_for_index'
+                                      end
                                 | _ ->
                                     cond_writes,
                                     ThreadSafetyDomain.PathDomain.join

infer/tests/codetoanalyze/java/threadsafety/Ownership.java

@@ -142,12 +142,12 @@ public class Ownership {
     writeToFormal(this.field);
   }
 
-  public void FP_writeToOwnedInCalleeIndirectOk1() {
+  public void writeToOwnedInCalleeIndirectOk1() {
     Obj o = new Obj();
     callWriteToFormal(o);
   }
 
-  public void FP_writeToOwnedInCalleeIndirectOk2() {
+  public void writeToOwnedInCalleeIndirectOk2() {
     Obj o = new Obj();
     o.g = new Obj();
     callWriteToFormal(o.g);

infer/tests/codetoanalyze/java/threadsafety/issues.exp

@@ -13,8 +13,6 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THRE
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Locks.f]
 codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownershipNotInterproceduralOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f]
-codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_writeToOwnedInCalleeIndirectOk1(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f]
-codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_writeToOwnedInCalleeIndirectOk2(), 3, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),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.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]