[racerd] remove redundant ownership constructor/state

Reviewed By: jeremydubreil

Differential Revision: D13489018

fbshipit-source-id: b94c50664

infer/src/concurrency/RacerD.ml

@@ -33,7 +33,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | access :: access_list -> (
           let prefix_path' = (fst prefix_path, snd prefix_path @ [access]) in
           let add_field_access pre =
-            let access_acc' = AccessDomain.add pre access_acc in
+            let access_acc' = AccessDomain.add_opt pre access_acc in
             add_field_accesses prefix_path' access_acc' access_list
           in
           if RacerDModels.is_safe_access access prefix_path proc_data.tenv then
@@ -49,17 +49,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     proc_data.pdesc
                 in
                 add_field_access pre
-            | OwnershipAbstractValue.Owned ->
-                add_field_accesses prefix_path' access_acc access_list
             | OwnershipAbstractValue.Unowned ->
                 let pre = AccessSnapshot.make access locks threads False proc_data.pdesc in
                 add_field_access pre )
     in
-    List.fold
-      ~f:(fun acc access_expr ->
+    List.fold (HilExp.get_access_exprs exp) ~init:accesses ~f:(fun acc access_expr ->
         let base, accesses = HilExp.AccessExpression.to_access_path access_expr in
         add_field_accesses (base, []) acc accesses )
-      ~init:accesses (HilExp.get_access_exprs exp)
 
 
   let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc
@@ -78,7 +74,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             (AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0))
             caller_pdesc
         in
-        AccessDomain.singleton snapshot
+        AccessDomain.add_opt snapshot AccessDomain.empty
     in
     (* if a container c is owned in cpp, make c[i] owned for all i *)
     let return_ownership =
@@ -148,12 +144,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         | None ->
             path
       in
-      let expand_precondition (snapshot : AccessSnapshot.t) =
-        let access' = TraceElem.map ~f:expand_path snapshot.access in
-        if phys_equal snapshot.access access' then snapshot
-        else AccessSnapshot.make_from_snapshot access' snapshot
+      let add snapshot acc =
+        let access' = TraceElem.map ~f:expand_path snapshot.AccessSnapshot.access in
+        let snapshot_opt' = AccessSnapshot.make_from_snapshot access' snapshot in
+        AccessDomain.add_opt snapshot_opt' acc
       in
-      AccessDomain.map expand_precondition accesses
+      AccessDomain.fold add accesses AccessDomain.empty
 
 
   let add_callee_accesses (caller_astate : Domain.t) callee_accesses locks threads actuals
@@ -168,10 +164,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | HilExp.AccessExpression access_expr -> (
           let actual_access_path = HilExp.AccessExpression.to_access_path access_expr in
           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)
@@ -214,8 +206,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         (* discard accesses to owned memory *)
         acc
       else
-        let snapshot = AccessSnapshot.make access locks thread ownership_precondition pdesc in
-        AccessDomain.add snapshot acc
+        let snapshot_opt = AccessSnapshot.make access locks thread ownership_precondition pdesc in
+        AccessDomain.add_opt snapshot_opt acc
     in
     AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses
 

infer/src/concurrency/RacerDDomain.ml

@@ -291,14 +291,16 @@ module AccessSnapshot = struct
   let make_from_snapshot access {lock; thread; ownership_precondition} =
     (* shouldn't be creating metadata for accesses that are known to be owned; we should discard
        such accesses *)
-    assert (not (OwnershipPrecondition.is_true ownership_precondition)) ;
-    {access; thread; lock; ownership_precondition}
+    Option.some_if
+      (not (OwnershipPrecondition.is_true ownership_precondition))
+      {access; thread; lock; ownership_precondition}
 
 
   let make access lock thread ownership_precondition pdesc =
-    assert (not (OwnershipPrecondition.is_true ownership_precondition)) ;
-    let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in
-    {access; lock; thread; ownership_precondition}
+    if not (OwnershipPrecondition.is_true ownership_precondition) then
+      let lock = LocksDomain.is_locked lock || Procdesc.is_java_synchronized pdesc in
+      Some {access; lock; thread; ownership_precondition}
+    else None
 
 
   let is_unprotected {thread; lock; ownership_precondition} =
@@ -321,12 +323,16 @@ module AccessDomain = struct
       |> Option.value_map ~default:false ~f:(fun ((v, _), _) -> should_skip_var v)
     in
     if skip then astate else add s astate
+
+
+  let add_opt snapshot_opt astate =
+    Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc)
 end
 
 module OwnershipAbstractValue = struct
-  type t = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare]
+  type t = OwnedIf of IntSet.t | Unowned [@@deriving compare]
 
-  let owned = Owned
+  let owned = OwnedIf IntSet.empty
 
   let unowned = Unowned
 
@@ -340,12 +346,8 @@ module OwnershipAbstractValue = struct
         true (* Unowned is top *)
     | Unowned, _ ->
         false
-    | Owned, _ ->
-        true (* Owned is bottom *)
     | OwnedIf s1, OwnedIf s2 ->
         IntSet.subset s1 s2
-    | OwnedIf _, Owned ->
-        false
 
 
   let join astate1 astate2 =
@@ -354,8 +356,6 @@ module OwnershipAbstractValue = struct
       match (astate1, astate2) with
       | _, Unowned | Unowned, _ ->
           Unowned
-      | astate, Owned | Owned, astate ->
-          astate
       | OwnedIf s1, OwnedIf s2 ->
           OwnedIf (IntSet.union s1 s2)
 
@@ -366,11 +366,11 @@ module OwnershipAbstractValue = struct
     | Unowned ->
         F.pp_print_string fmt "Unowned"
     | OwnedIf s ->
-        F.fprintf fmt "OwnedIf%a"
-          (PrettyPrintable.pp_collection ~pp_item:Int.pp)
-          (IntSet.elements s)
-    | Owned ->
-        F.pp_print_string fmt "Owned"
+        if IntSet.is_empty s then F.pp_print_string fmt "Owned"
+        else
+          F.fprintf fmt "OwnedIf%a"
+            (PrettyPrintable.pp_collection ~pp_item:Int.pp)
+            (IntSet.elements s)
 end
 
 module OwnershipDomain = struct
@@ -387,7 +387,7 @@ module OwnershipDomain = struct
           OwnershipAbstractValue.Unowned
     in
     match find access_path astate with
-    | (OwnershipAbstractValue.Owned | OwnedIf _) as v ->
+    | OwnershipAbstractValue.OwnedIf _ as v ->
         v
     | OwnershipAbstractValue.Unowned ->
         keep_looking access_path astate
@@ -426,7 +426,7 @@ module OwnershipDomain = struct
     in
     let ret_ownership_wrt_actuals =
       match return_ownership with
-      | OwnershipAbstractValue.Owned | Unowned ->
+      | OwnershipAbstractValue.Unowned ->
           return_ownership
       | OwnershipAbstractValue.OwnedIf formal_indexes ->
           IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned
@@ -595,4 +595,4 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} =
 let add_unannotated_call_access pname loc pdesc (astate : t) =
   let access = TraceElem.make_unannotated_call_access pname loc in
   let snapshot = AccessSnapshot.make access astate.locks astate.threads False pdesc in
-  {astate with accesses= AccessDomain.add snapshot astate.accesses}
+  {astate with accesses= AccessDomain.add_opt snapshot astate.accesses}

infer/src/concurrency/RacerDDomain.mli

@@ -116,9 +116,9 @@ module AccessSnapshot : sig
     -> ThreadsDomain.t
     -> OwnershipPrecondition.t
     -> Procdesc.t
-    -> t
+    -> t option
 
-  val make_from_snapshot : PathDomain.Sink.t -> t -> t
+  val make_from_snapshot : PathDomain.Sink.t -> t -> t option
 
   val is_unprotected : t -> bool
   (** return true if not protected by lock, thread, or ownership *)
@@ -126,12 +126,17 @@ end
 
 (** map of access metadata |-> set of accesses. the map should hold all accesses to a
     possibly-unowned access path *)
-module AccessDomain : AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t
+module AccessDomain : sig
+  include AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t
+
+  val add_opt : elt option -> t -> t
+end
 
 module OwnershipAbstractValue : sig
   type t = private
-    | Owned  (** Owned value; bottom of the lattice *)
-    | OwnedIf of IntSet.t  (** Owned if the formals at the given indexes are owned in the caller *)
+    | OwnedIf of IntSet.t
+        (** Owned if the formals at the given indexes are owned in the caller; unconditionally owned 
+        if the set of formals is empty = bottom of the lattice *)
     | Unowned  (** Unowned value; top of the lattice *)
   [@@deriving compare]