[racerd] significantly simplify deep ownership logic

Summary:
We had a semantics for ownership of prefix paths in mind (see comment), but it was enforced partially in the domain and partially in the transfer functions.
Moving all of the logic into the domain makes things much cleaner/shorter.

Reviewed By: ngorogiannis

Differential Revision: D7845981

fbshipit-source-id: 4a2da95

infer/src/concurrency/RacerD.ml

@@ -33,28 +33,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map
 
 
-  let propagate_ownership ((lhs_root, accesses) as lhs_access_path) rhs_exp ownership =
+  let propagate_ownership ((lhs_root, _) as lhs_access_path) rhs_exp ownership =
     if Var.is_global (fst lhs_root) then
       (* do not assign ownership to access paths rooted at globals *)
       ownership
     else
-      let ownership_value =
-        match accesses with
-        | [] ->
-            Domain.ownership_of_expr rhs_exp ownership
-        | [_]
-          when match Domain.OwnershipDomain.get_owned (lhs_root, []) ownership with
-               | Domain.OwnershipAbstractValue.OwnedIf _ ->
-                   true
-               | _ ->
-                   false ->
-            Domain.ownership_of_expr rhs_exp ownership
-        | _ when Domain.OwnershipDomain.is_owned lhs_access_path ownership ->
-            Domain.ownership_of_expr rhs_exp ownership
-        | _ ->
-            Domain.OwnershipAbstractValue.unowned
-      in
-      Domain.OwnershipDomain.add lhs_access_path ownership_value ownership
+      let rhs_ownership_value = Domain.ownership_of_expr rhs_exp ownership in
+      Domain.OwnershipDomain.add lhs_access_path rhs_ownership_value ownership
 
 
   let propagate_return return ret_ownership ret_attributes actuals
@@ -327,16 +312,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else
             let base = fst actual_access_path in
             match OwnershipDomain.get_owned (base, []) caller_astate.ownership with
-            | OwnedIf formal_indexes ->
-                (* the actual passed to the current callee is rooted in a formal *)
-                Conjunction (IntSet.union formal_indexes actual_indexes)
-            | Unowned | Owned ->
-              match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with
+            | Owned ->
+                (* the actual passed to the current callee is owned. drop all the conditional
+                   accesses for that actual, since they're all safe *)
+                Conjunction actual_indexes
             | OwnedIf formal_indexes ->
                 (* access path conditionally owned if [formal_indexes] are owned *)
                 Conjunction (IntSet.union formal_indexes actual_indexes)
-              | Owned ->
-                  assert false
             | Unowned ->
                 (* access path not rooted in a formal and not conditionally owned *)
                 False )

infer/src/concurrency/RacerDDomain.ml

@@ -329,38 +329,31 @@ end
 module OwnershipDomain = struct
   include AbstractDomain.Map (AccessPath) (OwnershipAbstractValue)
 
-  (* Helper function used by both is_owned and get_owned. Not exported.*)
-  let get_owned_shallow access_path astate =
-    try find access_path astate with Caml.Not_found -> OwnershipAbstractValue.Unowned
+  (* return the first non-Unowned ownership value found when checking progressively shorter
+     prefixes of [access_path] *)
+  let rec get_owned access_path astate =
+    let keep_looking access_path astate =
+      match AccessPath.truncate access_path with
+      | access_path', Some _ ->
+          get_owned access_path' astate
+      | _ ->
+          OwnershipAbstractValue.Unowned
+    in
+    match find access_path astate with
+    | (OwnershipAbstractValue.Owned | OwnedIf _) as v ->
+        v
+    | OwnershipAbstractValue.Unowned ->
+        keep_looking access_path astate
+    | exception Caml.Not_found ->
+        keep_looking access_path astate
 
 
-  (*deep ownership model where only a prefix needs to be owned in the astate*)
-  let is_owned (base, accesses) astate =
-    let is_owned_shallow access_path astate =
-      match get_owned_shallow access_path astate with
+  let is_owned access_path astate =
+    match get_owned access_path astate with
     | OwnershipAbstractValue.Owned ->
         true
-      | _ ->
+    | OwnershipAbstractValue.OwnedIf _ | Unowned ->
         false
-    in
-    let rec helper = function
-      | prefix, _ when is_owned_shallow (base, prefix) astate ->
-          true
-      | _, [] ->
-          false
-      | prefix, hd :: tl ->
-          helper (List.append prefix [hd], tl)
-    in
-    helper ([], accesses)
-
-
-  (*
-returns Owned if any prefix is owned on any prefix, else OwnedIf if it is
-OwnedIf in the astate, else UnOwned
-*)
-  let get_owned access_path astate =
-    if is_owned access_path astate then OwnershipAbstractValue.Owned
-    else try find access_path astate with Caml.Not_found -> OwnershipAbstractValue.Unowned
 
 
   let find = `Use_get_owned_instead