From 78521419a9ec03cdcbb8caf0abd5ec4e7693f82c Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Wed, 2 May 2018 09:09:14 -0700
Subject: [PATCH] [racerd] make deep ownership work with OwnedIf

Reviewed By: ngorogiannis

Differential Revision: D7844585

fbshipit-source-id: 96aedca
---
 infer/src/concurrency/RacerD.ml               |  5 +++--
 .../codetoanalyze/java/racerd/Builders.java   | 19 +++++++++++++++++++
 .../codetoanalyze/java/racerd/issues.exp      |  1 +
 3 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml
index 67c3ebd46..fbf8eba37 100644
--- a/infer/src/concurrency/RacerD.ml
+++ b/infer/src/concurrency/RacerD.ml
@@ -145,7 +145,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | _ ->
           false
     in
-    (* TODO: simplify this with AccessPath.truncate *)
     let rec add_field_accesses prefix_path access_acc = function
       | [] ->
           access_acc
@@ -160,7 +159,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else
             let is_write = if List.is_empty access_list then is_write_access else false in
             let access = TraceElem.make_field_access prefix_path' ~is_write loc in
-            match OwnershipDomain.get_owned prefix_path ownership with
+            (* use ownership value of base: if base is owned, treat suffixes as owned too *)
+            let base_path = (fst prefix_path, []) in
+            match OwnershipDomain.get_owned base_path ownership with
             | OwnershipAbstractValue.OwnedIf formal_indexes ->
                 let pre =
                   AccessSnapshot.make access locks threads
diff --git a/infer/tests/codetoanalyze/java/racerd/Builders.java b/infer/tests/codetoanalyze/java/racerd/Builders.java
index 5a954d770..94d4023bb 100644
--- a/infer/tests/codetoanalyze/java/racerd/Builders.java
+++ b/infer/tests/codetoanalyze/java/racerd/Builders.java
@@ -104,3 +104,22 @@ class TopLevelBuilder {
   }
 
 }
+
+class MyBuilder {
+  Obj mObj;
+
+  public static MyBuilder create() {
+    return new MyBuilder();
+  }
+
+  public MyBuilder setNestedPath(int i) {
+    this.mObj.f = i;
+    return this;
+  }
+
+  @ThreadSafe
+  static void setNestedPathOk(int i) {
+    MyBuilder.create().setNestedPath(1);
+  }
+
+}
diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp
index fae96dbdc..9effe24f6 100644
--- a/infer/tests/codetoanalyze/java/racerd/issues.exp
+++ b/infer/tests/codetoanalyze/java/racerd/issues.exp
@@ -81,6 +81,7 @@ codetoanalyze/java/racerd/Ownership.java, void Ownership.notPropagatingOwnership
 codetoanalyze/java/racerd/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignParamToUnownedBad(), 1, THREAD_SAFETY_VIOLATION, ERROR, [call to void Ownership.reassignParamToUnowned(Obj),access to `o.codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_VIOLATION, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.g`]
+codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.g.codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, ERROR, [<Read trace>,access to `formal.codetoanalyze.java.checkers.Obj.g`,<Write trace>,access to `formal.codetoanalyze.java.checkers.Obj.g`]
 codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad1(Obj), 1, THREAD_SAFETY_VIOLATION, ERROR, [call to void Ownership.writeToFormal(Obj),access to `formal.codetoanalyze.java.checkers.Obj.f`]
 codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, ERROR, [call to void Ownership.writeToFormal(Obj),access to `formal.codetoanalyze.java.checkers.Obj.f`]