[racerd] make deep ownership work with OwnedIf

Reviewed By: ngorogiannis

Differential Revision: D7844585

fbshipit-source-id: 96aedca

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

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

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`]