From c4c495fbe51d248b098ee47eaf117b1d179a34a3 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 19 Jan 2017 10:57:16 -0800
Subject: [PATCH] [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            | 29 +++++++++++++++++--
 .../java/threadsafety/Ownership.java          |  4 +--
 .../java/threadsafety/issues.exp              |  2 --
 3 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml
index 33f32842b..67ec183e0 100644
--- a/infer/src/checkers/ThreadSafety.ml
+++ b/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
diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java
index 280b2e6d9..d3bcb3e44 100644
--- a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java
+++ b/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);
diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp
index 707f5763d..26dd5bd4d 100644
--- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp
+++ b/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]