[racerd] remove ownership precondition module

Summary: This module mirrors `OwnershipAbstractValue`.  Its removal also allows simplifying `add_callee_accesses` significantly.

Reviewed By: jberdine

Differential Revision: D20563938

fbshipit-source-id: 36abca2d0

infer/src/concurrency/RacerD.ml

@@ -40,7 +40,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else
             let is_write = List.is_empty access_list && is_write_access in
             let access = TraceElem.make_field_access prefix_path' ~is_write loc in
-            let pre = OwnershipDomain.get_precondition prefix_path ownership in
+            let pre = OwnershipDomain.get_owned prefix_path ownership in
             let snapshot_opt = AccessSnapshot.make formals access locks threads pre in
             let access_acc' = AccessDomain.add_opt snapshot_opt acc in
             add_field_accesses prefix_path' access_acc' access_list
@@ -59,7 +59,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let container_access =
           TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc
         in
-        let ownership_pre = OwnershipDomain.get_precondition receiver_ap astate.ownership in
+        let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in
         AccessSnapshot.make formals container_access astate.locks astate.threads ownership_pre
       in
       let ownership_value = OwnershipDomain.get_owned receiver_ap astate.ownership in
@@ -118,33 +118,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals
       callee_pname loc =
     let open Domain in
-    let conjoin_ownership_precondition actual_indexes actual_exp :
-        AccessSnapshot.OwnershipPrecondition.t =
-      match actual_exp with
-      | HilExp.Constant _ ->
-          (* the actual is a constant, so it's owned in the caller. *)
-          Conjunction actual_indexes
-      | HilExp.AccessExpression access_expr -> (
-        match OwnershipDomain.get_owned access_expr caller_astate.ownership with
-        | OwnedIf formal_indexes ->
-            (* conditionally owned if [formal_indexes] are owned *)
-            Conjunction (IntSet.union formal_indexes actual_indexes)
-        | Unowned ->
-            (* not rooted in a formal and not conditionally owned *)
-            False )
-      | _ ->
-          (* couldn't find access expr, don't know if it's owned. assume not *)
-          False
-    in
-    let update_ownership_precondition actual_index (acc : AccessSnapshot.OwnershipPrecondition.t) =
+    let update_ownership_precondition actual_index (acc : OwnershipAbstractValue.t) =
       match acc with
-      | False ->
-          (* precondition can't be satisfied *)
+      | Unowned ->
+          (* optimisation -- already unowned, don't compute ownership of remaining actuals *)
+          acc
+      | actuals_ownership -> (
+        match List.nth actuals actual_index with
+        | None ->
+            (* vararg methods can result into missing actuals so simply ignore *)
             acc
-      | Conjunction actual_indexes ->
-          List.nth actuals actual_index
-          (* optional args can result into missing actuals so simply ignore *)
-          |> Option.value_map ~default:acc ~f:(conjoin_ownership_precondition actual_indexes)
+        | Some actual_exp ->
+            OwnershipDomain.ownership_of_expr actual_exp caller_astate.ownership
+            |> OwnershipAbstractValue.join actuals_ownership )
     in
     let update_callee_access (snapshot : AccessSnapshot.t) acc =
       let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in
@@ -155,18 +141,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       (* update precondition with caller ownership info *)
       let ownership_precondition =
         match snapshot.ownership_precondition with
-        | Conjunction indexes ->
-            let empty_precondition =
-              AccessSnapshot.OwnershipPrecondition.Conjunction IntSet.empty
-            in
-            IntSet.fold update_ownership_precondition indexes empty_precondition
-        | False ->
+        | OwnedIf indexes ->
+            IntSet.fold update_ownership_precondition indexes OwnershipAbstractValue.owned
+        | Unowned ->
             snapshot.ownership_precondition
       in
-      if AccessSnapshot.OwnershipPrecondition.is_true ownership_precondition then
-        (* discard accesses to owned memory *)
-        acc
-      else
       let snapshot_opt = AccessSnapshot.make formals access locks thread ownership_precondition in
       AccessDomain.add_opt snapshot_opt acc
     in

infer/src/concurrency/RacerDDomain.ml

@@ -260,32 +260,63 @@ module ThreadsDomain = struct
     match callee_astate with AnyThreadButSelf -> callee_astate | _ -> caller_astate
 end
 
-module AccessSnapshot = struct
-  module OwnershipPrecondition = struct
-    type t = Conjunction of IntSet.t | False [@@deriving compare]
+module OwnershipAbstractValue = struct
+  type t = OwnedIf of IntSet.t | Unowned [@@deriving compare]
+
+  let owned = OwnedIf IntSet.empty
+
+  let is_owned = function OwnedIf set -> IntSet.is_empty set | _ -> false
 
-    (* precondition is true if the conjunction of owned indexes is empty *)
-    let is_true = function False -> false | Conjunction set -> IntSet.is_empty set
+  let unowned = Unowned
+
+  let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index)
+
+  let leq ~lhs ~rhs =
+    phys_equal lhs rhs
+    ||
+    match (lhs, rhs) with
+    | _, Unowned ->
+        true (* Unowned is top *)
+    | Unowned, _ ->
+        false
+    | OwnedIf s1, OwnedIf s2 ->
+        IntSet.subset s1 s2
+
+
+  let join astate1 astate2 =
+    if phys_equal astate1 astate2 then astate1
+    else
+      match (astate1, astate2) with
+      | _, Unowned | Unowned, _ ->
+          Unowned
+      | OwnedIf s1, OwnedIf s2 ->
+          OwnedIf (IntSet.union s1 s2)
+
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
 
   let pp fmt = function
-      | Conjunction indexes ->
-          F.fprintf fmt "Owned(%a)"
+    | Unowned ->
+        F.pp_print_string fmt "Unowned"
+    | OwnedIf s ->
+        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 indexes)
-      | False ->
-          F.pp_print_string fmt "False"
-  end
+            (IntSet.elements s)
+end
 
+module AccessSnapshot = struct
   type t =
     { access: TraceElem.t
     ; thread: ThreadsDomain.t
     ; lock: bool
-    ; ownership_precondition: OwnershipPrecondition.t }
+    ; ownership_precondition: OwnershipAbstractValue.t }
   [@@deriving compare]
 
   let make_if_not_owned formals access lock thread ownership_precondition =
     if
-      (not (OwnershipPrecondition.is_true ownership_precondition))
+      (not (OwnershipAbstractValue.is_owned ownership_precondition))
       && TraceElem.should_keep formals access
     then Some {access; lock; thread; ownership_precondition}
     else None
@@ -303,13 +334,13 @@ module AccessSnapshot = struct
   let is_unprotected {thread; lock; ownership_precondition} =
     (not (ThreadsDomain.is_any_but_self thread))
     && (not lock)
-    && not (OwnershipPrecondition.is_true ownership_precondition)
+    && not (OwnershipAbstractValue.is_owned ownership_precondition)
 
 
   let pp fmt {access; thread; lock; ownership_precondition} =
     F.fprintf fmt "Loc: %a Access: %a Thread: %a Lock: %b Pre: %a" Location.pp
       (TraceElem.get_loc access) TraceElem.pp access ThreadsDomain.pp thread lock
-      OwnershipPrecondition.pp ownership_precondition
+      OwnershipAbstractValue.pp ownership_precondition
 end
 
 module AccessDomain = struct
@@ -327,50 +358,6 @@ module AccessDomain = struct
     Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc)
 end
 
-module OwnershipAbstractValue = struct
-  type t = OwnedIf of IntSet.t | Unowned [@@deriving compare]
-
-  let owned = OwnedIf IntSet.empty
-
-  let unowned = Unowned
-
-  let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index)
-
-  let leq ~lhs ~rhs =
-    phys_equal lhs rhs
-    ||
-    match (lhs, rhs) with
-    | _, Unowned ->
-        true (* Unowned is top *)
-    | Unowned, _ ->
-        false
-    | OwnedIf s1, OwnedIf s2 ->
-        IntSet.subset s1 s2
-
-
-  let join astate1 astate2 =
-    if phys_equal astate1 astate2 then astate1
-    else
-      match (astate1, astate2) with
-      | _, Unowned | Unowned, _ ->
-          Unowned
-      | OwnedIf s1, OwnedIf s2 ->
-          OwnedIf (IntSet.union s1 s2)
-
-
-  let widen ~prev ~next ~num_iters:_ = join prev next
-
-  let pp fmt = function
-    | Unowned ->
-        F.pp_print_string fmt "Unowned"
-    | OwnedIf s ->
-        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
   include AbstractDomain.Map (AccessExpression) (OwnershipAbstractValue)
 
@@ -426,16 +413,6 @@ module OwnershipDomain = struct
           IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned
     in
     add ret_access_exp ret_ownership_wrt_actuals ownership
-
-
-  let get_precondition exp t =
-    match get_owned exp t with
-    | OwnedIf formal_indexes ->
-        (* access expression conditionally owned if [formal_indexes] are owned *)
-        AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes
-    | Unowned ->
-        (* access expression not rooted in a formal and not conditionally owned *)
-        AccessSnapshot.OwnershipPrecondition.False
 end
 
 module Attribute = struct
@@ -582,5 +559,5 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} =
 
 let add_unannotated_call_access formals pname loc (astate : t) =
   let access = TraceElem.make_unannotated_call_access pname loc in
-  let snapshot = AccessSnapshot.make formals access astate.locks astate.threads False in
+  let snapshot = AccessSnapshot.make formals access astate.locks astate.threads Unowned in
   {astate with accesses= AccessDomain.add_opt snapshot astate.accesses}

infer/src/concurrency/RacerDDomain.mli

@@ -83,27 +83,30 @@ module ThreadsDomain : sig
   (** integrate current state with a callee summary *)
 end
 
-(** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held,
-    ownership precondition *)
-module AccessSnapshot : sig
-  (** precondition for owned access; access is owned if it evaluates to true *)
-  module OwnershipPrecondition : sig
-    type t =
-      | Conjunction of IntSet.t
-          (** Conjunction of "formal index must be owned" predicates. true if empty *)
-      | False
+module OwnershipAbstractValue : sig
+  type t = private
+    | 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 *)
 
-    include PrettyPrintable.PrintableOrderedType with type t := t
+  val owned : t
 
-    val is_true : t -> bool
-    (** return [true] if the precondition evaluates to true *)
-  end
+  val is_owned : t -> bool
+
+  val make_owned_if : int -> t
+
+  val join : t -> t -> t
+end
 
+(** snapshot of the relevant state at the time of a heap access: concurrent thread(s), lock(s) held,
+    ownership precondition *)
+module AccessSnapshot : sig
   type t = private
     { access: TraceElem.t
     ; thread: ThreadsDomain.t
     ; lock: bool
-    ; ownership_precondition: OwnershipPrecondition.t }
+    ; ownership_precondition: OwnershipAbstractValue.t }
 
   include PrettyPrintable.PrintableOrderedType with type t := t
 
@@ -112,7 +115,7 @@ module AccessSnapshot : sig
     -> TraceElem.t
     -> LocksDomain.t
     -> ThreadsDomain.t
-    -> OwnershipPrecondition.t
+    -> OwnershipAbstractValue.t
     -> t option
 
   val make_from_snapshot : FormalMap.t -> TraceElem.t -> t -> t option
@@ -129,19 +132,6 @@ module AccessDomain : sig
   val add_opt : elt option -> t -> t
 end
 
-module OwnershipAbstractValue : sig
-  type t = private
-    | 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]
-
-  val owned : t
-
-  val make_owned_if : int -> t
-end
-
 module OwnershipDomain : sig
   type t
 
@@ -155,7 +145,7 @@ module OwnershipDomain : sig
 
   val propagate_return : AccessExpression.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t
 
-  val get_precondition : AccessExpression.t -> t -> AccessSnapshot.OwnershipPrecondition.t
+  val ownership_of_expr : HilExp.t -> t -> OwnershipAbstractValue.t
 end
 
 module Attribute : sig