From d0ee36b3a8efb7179fa38e1435504a799116721e Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 10 Aug 2017 10:01:03 -0700
Subject: [PATCH] [thread-safety] add ownership domain: map of access paths to
 a lattice of ownership predicates

Summary: Stepping stone to a more precise ownership domain.

Reviewed By: jberdine

Differential Revision: D5589834

fbshipit-source-id: 4f6c24a
---
 infer/src/checkers/ThreadSafetyDomain.ml  | 60 +++++++++++++++++++++++
 infer/src/checkers/ThreadSafetyDomain.mli | 27 ++++++++++
 2 files changed, 87 insertions(+)

diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml
index b49467da6..2d1aa9f6e 100644
--- a/infer/src/checkers/ThreadSafetyDomain.ml
+++ b/infer/src/checkers/ThreadSafetyDomain.ml
@@ -149,6 +149,66 @@ end
 
 module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set)
 
+module OwnershipAbstractValue = struct
+  type astate = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare]
+
+  let owned = Owned
+
+  let unowned = Unowned
+
+  let make_owned_if formal_index = OwnedIf (IntSet.singleton formal_index)
+
+  let ( <= ) ~lhs ~rhs =
+    if phys_equal lhs rhs then true
+    else
+      match (lhs, rhs) with
+      | _, Unowned
+       -> 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 =
+    if phys_equal astate1 astate2 then astate1
+    else
+      match (astate1, astate2) with
+      | _, Unowned | Unowned, _
+       -> Unowned
+      | astate, Owned | Owned, astate
+       -> astate
+      | OwnedIf s1, OwnedIf s2
+       -> OwnedIf (IntSet.union s1 s2)
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+
+  let pp fmt = function
+    | Unowned
+     -> F.fprintf fmt "Unowned"
+    | OwnedIf s
+     -> F.fprintf fmt "OwnedIf%a" (PrettyPrintable.pp_collection ~pp_item:Int.pp)
+          (IntSet.elements s)
+    | Owned
+     -> F.fprintf fmt "Owned"
+end
+
+module OwnershipDomain = struct
+  include AbstractDomain.Map (AccessPath) (OwnershipAbstractValue)
+
+  let get_owned access_path astate =
+    try find access_path astate
+    with Not_found -> OwnershipAbstractValue.Unowned
+
+  let is_owned access_path astate =
+    match get_owned access_path astate with OwnershipAbstractValue.Owned -> true | _ -> false
+
+  let find = `Use_get_owned_instead
+end
+
 module AttributeMapDomain = struct
   include AbstractDomain.InvertedMap (AccessPath.Map) (AttributeSetDomain)
 
diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli
index a272418b3..942b32cac 100644
--- a/infer/src/checkers/ThreadSafetyDomain.mli
+++ b/infer/src/checkers/ThreadSafetyDomain.mli
@@ -48,6 +48,33 @@ module ThumbsUpDomain : AbstractDomain.S with type astate = bool
 
 module PathDomain : module type of SinkTrace.Make (TraceElem)
 
+(** Powerset domain on the formal indexes in OwnedIf with a distinguished bottom element (Owned) and top element (Unowned) *)
+module OwnershipAbstractValue : sig
+  type astate = 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 *)
+    | Unowned  (** Unowned value; top of the lattice *)
+    [@@deriving compare]
+
+  val owned : astate
+
+  val unowned : astate
+
+  val make_owned_if : int -> astate
+
+  include AbstractDomain.S with type astate := astate
+end
+
+module OwnershipDomain : sig
+  include module type of AbstractDomain.Map (AccessPath) (OwnershipAbstractValue)
+
+  val get_owned : AccessPath.t -> astate -> OwnershipAbstractValue.astate
+
+  val is_owned : AccessPath.t -> astate -> bool
+
+  val find : [`Use_get_owned_instead]
+end
+
 (** attribute attached to a boolean variable specifying what it means when the boolean is true *)
 module Choice : sig
   type t =