[thread-safety] eliminate escape analysis

Reviewed By: ngorogiannis

Differential Revision: D5946570

fbshipit-source-id: 9cd3509

infer/src/checkers/ThreadSafety.ml

@@ -499,7 +499,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       | _
        -> false
 
-  let make_container_access callee_pname ~is_write actuals receiver_ap callee_loc tenv =
+  let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv =
     (* create a dummy write that represents mutating the contents of the container *)
     let open Domain in
     let callee_accesses =
@@ -511,18 +511,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         AccessDomain.add_access (Unprotected (IntSet.singleton 0)) container_access
           AccessDomain.empty
     in
-    (* TODO: for now all formals escape *)
+    (* we need a more intelligent escape analysis, that branches on whether we own the container *)
-    (* we need a more intelligent escape analysis, that branches on whether
-             we own the container *)
-    let escapee_formals = List.length actuals |> List.range 0 |> FormalsDomain.of_list in
     Some
       { thumbs_up= true
       ; locks= false
       ; threads= ThreadsDomain.Unknown
       ; accesses= callee_accesses
       ; return_ownership= OwnershipAbstractValue.unowned
-      ; return_attributes= AttributeSetDomain.empty
+      ; return_attributes= AttributeSetDomain.empty }
-      ; escapee_formals }
 
   let get_summary caller_pdesc callee_pname actuals callee_loc tenv =
     let get_receiver_ap actuals =
@@ -536,11 +532,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     match get_container_access callee_pname tenv with
     | Some ContainerWrite
-     -> make_container_access callee_pname ~is_write:true actuals (get_receiver_ap actuals)
+     -> make_container_access callee_pname ~is_write:true (get_receiver_ap actuals) callee_loc tenv
-          callee_loc tenv
     | Some ContainerRead
-     -> make_container_access callee_pname ~is_write:false actuals (get_receiver_ap actuals)
+     -> make_container_access callee_pname ~is_write:false (get_receiver_ap actuals) callee_loc
-          callee_loc tenv
+          tenv
     | None
      -> Summary.read_summary caller_pdesc callee_pname
 
@@ -565,19 +560,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         add_access exp loc ~is_write_access:false acc locks threads ownership proc_data)
       exps ~init:accesses
 
-  let add_escapees_from_exp rhs_exp ownership escapees =
-    HilExp.get_access_paths rhs_exp |> List.rev_map ~f:(Domain.Escapee.of_access_path ownership)
-    |> List.concat_no_order |> Domain.EscapeeDomain.add_from_list escapees
-
-  let add_escapees_from_exp_list exp_list extras escapees =
-    List.fold ~init:escapees exp_list ~f:(fun acc exp -> add_escapees_from_exp exp extras acc)
-
-  let add_escapees_from_call actuals escapee_formals extras escapees =
-    let escapee_actuals =
-      Domain.FormalsDomain.elements escapee_formals |> List.rev_map ~f:(List.nth_exn actuals)
-    in
-    add_escapees_from_exp_list escapee_actuals extras escapees
-
   let exec_instr (astate: Domain.astate) ({ProcData.tenv; pdesc} as proc_data) _
       (instr: HilInstr.t) =
     let open Domain in
@@ -590,9 +572,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         let ownership =
           OwnershipDomain.add (ret_base, []) OwnershipAbstractValue.owned astate.ownership
         in
-        (* TODO: we need to model escaping formals, now just assume all escape *)
+        {astate with accesses; ownership}
-        let escapees = add_escapees_from_exp_list actuals astate.ownership astate.escapees in
-        {astate with accesses; ownership; escapees}
     | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc)
      -> (
         let accesses_with_unannotated_calls =
@@ -649,14 +629,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                     Typ.Procname.pp callee_pname )
             | NoEffect ->
               match get_summary pdesc callee_pname actuals loc tenv with
-              | Some
+              | Some {thumbs_up; threads; locks; accesses; return_ownership; return_attributes}
-                  { thumbs_up
-                  ; threads
-                  ; locks
-                  ; accesses
-                  ; return_ownership
-                  ; return_attributes
-                  ; escapee_formals }
                -> let update_caller_accesses pre callee_accesses caller_accesses =
                     let combined_accesses =
                       PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
@@ -735,17 +708,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   let ownership, attribute_map =
                     propagate_return ret_opt return_ownership return_attributes actuals astate
                   in
-                  let escapees =
+                  {thumbs_up; locks; threads; accesses; ownership; attribute_map}
-                    add_escapees_from_call actuals escapee_formals astate.ownership astate.escapees
-                  in
-                  {thumbs_up; locks; threads; accesses; ownership; attribute_map; escapees}
               | None
-               -> (* TODO: assume actuals escape, should we? *)
+               -> let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
-                  let new_escapees =
-                    add_escapees_from_exp_list actuals astate.ownership astate.escapees
-                  in
-                  let astate = {astate with escapees= new_escapees} in
-                  let should_assume_returns_ownership (call_flags: CallFlags.t) actuals =
                     (* assume non-interface methods with no summary and no parameters return
                          ownership *)
                     not call_flags.cf_interface && List.is_empty actuals
@@ -828,12 +793,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         in
         let ownership = propagate_ownership lhs_access_path rhs_exp astate.ownership in
         let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in
-        (* assigning to the return variable leads to no new escapees *)
+        {astate with accesses; ownership; attribute_map}
-        let escapees =
-          if fst lhs_access_path |> fst |> Var.is_return then astate.escapees
-          else add_escapees_from_exp rhs_exp astate.ownership astate.escapees
-        in
-        {astate with accesses; ownership; attribute_map; escapees}
     | Assume (assume_exp, _, _, loc)
      -> let rec eval_binop op var e1 e2 =
           match (eval_bexp var e1, eval_bexp var e2) with
@@ -992,8 +952,7 @@ let empty_post : ThreadSafetyDomain.summary =
   ; locks= false
   ; accesses= ThreadSafetyDomain.AccessDomain.empty
   ; return_ownership= ThreadSafetyDomain.OwnershipAbstractValue.unowned
-  ; return_attributes= ThreadSafetyDomain.AttributeSetDomain.empty
+  ; return_attributes= ThreadSafetyDomain.AttributeSetDomain.empty }
-  ; escapee_formals= ThreadSafetyDomain.FormalsDomain.empty }
 
 let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
   let is_initializer tenv proc_name =
@@ -1045,7 +1004,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
         ({ThreadSafetyDomain.empty with ownership; threads}, IdAccessPathMapDomain.empty)
     in
     match Analyzer.compute_post proc_data ~initial ~debug:false with
-    | Some ({thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}, _)
+    | Some ({thumbs_up; threads; locks; accesses; ownership; attribute_map}, _)
      -> let return_var_ap =
           AccessPath.of_pvar
             (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
@@ -1056,16 +1015,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
           try AttributeMapDomain.find return_var_ap attribute_map
           with Not_found -> AttributeSetDomain.empty
         in
-        let escapee_formals = FormalsDomain.of_escapees escapees in
+        let post = {thumbs_up; threads; locks; accesses; return_ownership; return_attributes} in
-        let post =
-          { thumbs_up
-          ; threads
-          ; locks
-          ; accesses
-          ; return_ownership
-          ; return_attributes
-          ; escapee_formals }
-        in
         Summary.update_summary post summary
     | None
      -> summary )

infer/src/checkers/ThreadSafetyDomain.ml

@@ -328,48 +328,13 @@ module AccessDomain = struct
     with Not_found -> PathDomain.empty
 end
 
-module Escapee = struct
-  type t = Formal of int | Local of Var.t [@@deriving compare]
-
-  let pp fmt = function
-    | Formal fml
-     -> F.fprintf fmt "Formal(%d)" fml
-    | Local loc
-     -> F.fprintf fmt "Local(%a)" Var.pp loc
-
-  let of_access_path ownership (base, _) =
-    match OwnershipDomain.get_owned (base, []) ownership with
-    | OwnershipAbstractValue.OwnedIf formal_indexes
-     -> List.map ~f:(fun formal_index -> Formal formal_index) (IntSet.elements formal_indexes)
-    | _
-     -> [Local (fst base)]
-end
-
-module EscapeeDomain = struct
-  include AbstractDomain.FiniteSet (Escapee)
-
-  let add_from_list escapees escapee_list =
-    List.fold ~init:escapees escapee_list ~f:(fun acc v -> add v acc)
-end
-
-module FormalsDomain = struct
-  include AbstractDomain.FiniteSet (Int)
-
-  let of_escapees escapees =
-    let aux escapee acc =
-      match escapee with Escapee.Formal fml -> add fml acc | Escapee.Local _ -> acc
-    in
-    EscapeeDomain.fold aux escapees empty
-end
-
 type astate =
   { thumbs_up: ThumbsUpDomain.astate
   ; threads: ThreadsDomain.astate
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; ownership: OwnershipDomain.astate
-  ; attribute_map: AttributeMapDomain.astate
+  ; attribute_map: AttributeMapDomain.astate }
-  ; escapees: EscapeeDomain.astate }
 
 let empty =
   let thumbs_up = true in
@@ -378,13 +343,11 @@ let empty =
   let accesses = AccessDomain.empty in
   let ownership = OwnershipDomain.empty in
   let attribute_map = AttributeMapDomain.empty in
-  let escapees = EscapeeDomain.empty in
+  {thumbs_up; threads; locks; accesses; ownership; attribute_map}
-  {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}
 
-let is_empty {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees} =
+let is_empty {thumbs_up; threads; locks; accesses; ownership; attribute_map} =
   thumbs_up && ThreadsDomain.is_unknown threads && not locks && AccessDomain.is_empty accesses
   && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map
-  && EscapeeDomain.is_empty escapees
 
 let ( <= ) ~lhs ~rhs =
   if phys_equal lhs rhs then true
@@ -392,7 +355,6 @@ let ( <= ) ~lhs ~rhs =
     && LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks
     && AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses
     && AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map
-    && EscapeeDomain.( <= ) ~lhs:lhs.escapees ~rhs:rhs.escapees
 
 let join astate1 astate2 =
   if phys_equal astate1 astate2 then astate1
@@ -403,8 +365,7 @@ let join astate1 astate2 =
     let accesses = AccessDomain.join astate1.accesses astate2.accesses in
     let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in
     let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
-    let escapees = EscapeeDomain.join astate1.escapees astate2.escapees in
+    {thumbs_up; threads; locks; accesses; ownership; attribute_map}
-    {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}
 
 let widen ~prev ~next ~num_iters =
   if phys_equal prev next then prev
@@ -417,8 +378,7 @@ let widen ~prev ~next ~num_iters =
     let attribute_map =
       AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters
     in
-    let escapees = EscapeeDomain.widen ~prev:prev.escapees ~next:next.escapees ~num_iters in
+    {thumbs_up; threads; locks; accesses; ownership; attribute_map}
-    {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}
 
 type summary =
   { thumbs_up: ThumbsUpDomain.astate
@@ -426,20 +386,16 @@ type summary =
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; return_ownership: OwnershipAbstractValue.astate
-  ; return_attributes: AttributeSetDomain.astate
+  ; return_attributes: AttributeSetDomain.astate }
-  ; escapee_formals: FormalsDomain.astate }
 
-let pp_summary fmt
+let pp_summary fmt {thumbs_up; threads; locks; accesses; return_ownership; return_attributes} =
-    {thumbs_up; threads; locks; accesses; return_ownership; return_attributes; escapee_formals} =
   F.fprintf fmt
-    "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\nEscapee Formals: %a @\n"
+    "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n"
     ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp
     accesses OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes
-    FormalsDomain.pp escapee_formals
 
-let pp fmt {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees} =
+let pp fmt {thumbs_up; threads; locks; accesses; ownership; attribute_map} =
   F.fprintf fmt
-    "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\nEscapees: %a @\n"
+    "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\n Ownership: %a @\nAttributes: %a @\n"
     ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp
-    accesses OwnershipDomain.pp ownership AttributeMapDomain.pp attribute_map EscapeeDomain.pp
+    accesses OwnershipDomain.pp ownership AttributeMapDomain.pp attribute_map
-    escapees

infer/src/checkers/ThreadSafetyDomain.mli

@@ -164,29 +164,6 @@ module AccessDomain : sig
   (** get all accesses with the given precondition *)
 end
 
-(** a formal or a local variable that may escape *)
-module Escapee : sig
-  type t = Formal of int | Local of Var.t [@@deriving compare]
-
-  val pp : F.formatter -> t -> unit
-
-  val of_access_path : OwnershipDomain.astate -> AccessPath.t -> t list
-end
-
-(** set of formals or locals that may escape *)
-module EscapeeDomain : sig
-  include module type of AbstractDomain.FiniteSet (Escapee)
-
-  val add_from_list : astate -> Escapee.t list -> astate
-end
-
-(** Domain that only includes escaping formals, for use in summary *)
-module FormalsDomain : sig
-  include module type of AbstractDomain.FiniteSet (Int)
-
-  val of_escapees : EscapeeDomain.astate -> astate
-end
-
 type astate =
   { thumbs_up: ThumbsUpDomain.astate  (** boolean that is true if we think we have a proof *)
   ; threads: ThreadsDomain.astate  (** current thread: main, background, or unknown *)
@@ -195,8 +172,7 @@ type astate =
         (** read and writes accesses performed without ownership permissions *)
   ; ownership: OwnershipDomain.astate  (** map of access paths to ownership predicates *)
   ; attribute_map: AttributeMapDomain.astate
-        (** map of access paths to attributes such as owned, functional, ... *)
+        (** map of access paths to attributes such as owned, functional, ... *) }
-  ; escapees: EscapeeDomain.astate  (** set of formals and locals that may escape *) }
 
 (** same as astate, but without [attribute_map] (since these involve locals) and with the addition
     of the ownership/attributes associated with the return value as well as the set of formals which
@@ -207,8 +183,7 @@ type summary =
   ; locks: LocksDomain.astate
   ; accesses: AccessDomain.astate
   ; return_ownership: OwnershipAbstractValue.astate
-  ; return_attributes: AttributeSetDomain.astate
+  ; return_attributes: AttributeSetDomain.astate }
-  ; escapee_formals: FormalsDomain.astate }
 
 include AbstractDomain.WithBottom with type astate := astate