[ownership] domain for borrowing

Summary:
Enrich capability domain with borrowing info. Inline comments explain what the domain is doing.

The analyzer isn't actually using the borrowing functionality yet--that comes in the successor.

Reviewed By: jeremydubreil

Differential Revision: D7067942

fbshipit-source-id: 4c03c69

infer/src/checkers/Ownership.ml

@@ -10,48 +10,59 @@
 open! IStd
 module F = Format
 module L = Logging
+module VarSet = AbstractDomain.FiniteSet (Var)
 
-type permission =
+module CapabilityDomain = struct
-  | TransferOwnership
+  type astate =
-      (** permission to permanently transfer ownership (e.g. call a destructor, delete, or free) *)
+    | Invalid  (** neither owned nor borrowed; we can't do anything with this value *)
-  | Read  (** permission to read *)
+    | BorrowedFrom of VarSet.astate
-
+        (** not owned, but borrowed from existing reference(s). for now, permits both reads and writes *)
-module Permission = struct
+    | Owned
-  type astate = permission
+        (** owned. permits reads, writes, and ownership transfer (e.g. call a destructor, delete, or free) *)
 
+  (** Owned <= BorrowedFrom <= Invalid *)
   let ( <= ) ~lhs ~rhs =
     match (lhs, rhs) with
-    | Read, TransferOwnership ->
+    | _, Invalid ->
         true
-    | Read, Read | TransferOwnership, TransferOwnership ->
+    | Invalid, _ ->
+        false
+    | BorrowedFrom s1, BorrowedFrom s2 ->
+        VarSet.( <= ) ~lhs:s1 ~rhs:s2
+    | Owned, _ ->
         true
-    | TransferOwnership, Read ->
+    | _, Owned ->
         false
 
 
   let join astate1 astate2 =
-    match (astate1, astate2) with
+    if phys_equal astate1 astate2 then astate1
-    | Read, Read ->
+    else
-        Read
+      match (astate1, astate2) with
-    | TransferOwnership, _ | _, TransferOwnership ->
+      | BorrowedFrom s1, BorrowedFrom s2 ->
-        TransferOwnership
+          BorrowedFrom (VarSet.union s1 s2)
+      | Owned, astate | astate, Owned ->
+          astate
+      | Invalid, _ | _, Invalid ->
+          Invalid
 
 
   let widen ~prev ~next ~num_iters:_ = join prev next
 
   let pp fmt = function
-    | TransferOwnership ->
+    | Invalid ->
-        F.fprintf fmt "TransferOwnership"
+        F.fprintf fmt "Invalid"
-    | Read ->
+    | BorrowedFrom vars ->
-        F.fprintf fmt "Read"
+        F.fprintf fmt "BorrowedFrom(%a)" VarSet.pp vars
+    | Owned ->
+        F.fprintf fmt "Owned"
 end
 
-(** map from variable to permission required based on the way the variable is used. for example, if
+(** map from program variable to its capability *)
-    we see delete x, then x needs permission "TransferOwnership" *)
 module Domain = struct
-  include AbstractDomain.Map (Var) (Permission)
+  include AbstractDomain.Map (Var) (CapabilityDomain)
 
-  let log_use_after_lifetime var loc summary =
+  let report_use_after_lifetime var loc summary =
     let message =
       F.asprintf "Variable %a is used after its lifetime has ended at %a" Var.pp var Location.pp
         loc
@@ -61,24 +72,35 @@ module Domain = struct
     Reporting.log_error summary ~loc ~ltr exn
 
 
-  (* don't allow strong updates via add; only remove *)
+  (* complain if we do not have the right capability to access [var] *)
-  let add var new_permission loc summary astate =
+  let check_var_lifetime var loc summary astate =
-    let permission =
+    let open CapabilityDomain in
-      try
+    match find var astate with
-        let old_permission = find var astate in
+    | Invalid ->
-        ( match (old_permission, new_permission) with
+        report_use_after_lifetime var loc summary
-        | TransferOwnership, (Read | TransferOwnership) ->
+    | BorrowedFrom borrowed_vars ->
-            log_use_after_lifetime var loc summary
+        (* warn if any of the borrowed vars are Invalid *)
-        | _ ->
+        let is_invalid v =
-            () ) ;
+          match find v astate with
-        Permission.join new_permission old_permission
+          | Invalid ->
-      with Not_found -> new_permission
+              true
-    in
+          | BorrowedFrom _
-    add var permission astate
+          (* TODO: can do deeper checking here, but have to worry about borrow cycles *)
+          | Owned ->
+              false
+          | exception Not_found ->
+              false
+        in
+        if VarSet.exists is_invalid borrowed_vars then report_use_after_lifetime var loc summary
+    | Owned ->
+        ()
+    | exception Not_found ->
+        ()
 
 
   let access_path_add_read ((base_var, _), _) loc summary astate =
-    add base_var Read loc summary astate
+    check_var_lifetime base_var loc summary astate ;
+    astate
 
 
   let exp_add_reads exp loc summary astate =
@@ -128,7 +150,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         |> Domain.access_path_add_read (AccessExpression.to_access_path lhs_access_exp) loc summary
     | Call (_, Direct callee_pname, [(AccessExpression Base (lhs_var, _))], _, loc)
       when transfers_ownership callee_pname ->
-        Domain.add lhs_var TransferOwnership loc summary astate
+        Domain.check_var_lifetime lhs_var loc summary astate ;
+        Domain.add lhs_var CapabilityDomain.Invalid astate
     | Call (_, Direct callee_pname, [(AccessExpression Base (lhs_var, _)); rhs_exp], _, loc)
       when String.equal (Typ.Procname.get_method callee_pname) "operator=" ->
         Domain.handle_var_assign lhs_var rhs_exp loc summary astate
@@ -142,7 +165,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           | _ ->
               L.die InternalError "Unexpected: constructor called on %a" HilExp.pp lhs_exp
         in
-        Domain.actuals_add_reads actuals loc summary astate |> Domain.remove constructed_var
+        Domain.actuals_add_reads actuals loc summary astate
+        |> Domain.add constructed_var CapabilityDomain.Owned
     | Call (ret_opt, _, actuals, _, loc)
       -> (
         let astate' = Domain.actuals_add_reads actuals loc summary astate in