[retain cycles] Refactoring of computing cycles using dedicated data structure

Reviewed By: mbouaziz

Differential Revision: D6534576

fbshipit-source-id: 119b618

infer/src/IR/Localise.ml

@@ -891,41 +891,34 @@ let desc_return_expression_required typ_str loc =
 
 let desc_retain_cycle cycle loc cycle_dotty =
   Logging.d_strln "Proposition with retain cycle:" ;
-  let ct = ref 1 in
   let tags = Tags.create () in
-  let str_cycle = ref "" in
+  let desc_retain_cycle (cycle: RetainCyclesType.t) =
+    let open RetainCyclesType in
     let remove_old s =
       match Str.split_delim (Str.regexp_string "&old_") s with [_; s'] -> s' | _ -> s
     in
-  let do_edge ((se, _), f, _) =
+    let do_edge index_ edge =
-    match se with
+      let index = index_ + 1 in
-    | Sil.Eexp (Exp.Lvar pvar, _) when Pvar.equal pvar Sil.block_pvar ->
+      let from_exp_str =
-        str_cycle
+        match edge.rc_from.rc_node_exp with
-        := !str_cycle ^ " (" ^ string_of_int !ct ^ ") a block capturing "
+        | Exp.Lvar pvar when Pvar.equal pvar Sil.block_pvar ->
-           ^ MF.monospaced_to_string (Typ.Fieldname.to_string f) ^ "; " ;
+            "a block capturing"
-        ct := !ct + 1
+        | Exp.Lvar pvar as e ->
-    | Sil.Eexp ((Exp.Lvar pvar as e), _) ->
             let e_str = Exp.to_string e in
-        let e_str = if Pvar.is_seed pvar then remove_old e_str else e_str in
+            if Pvar.is_seed pvar then remove_old e_str else e_str
-        str_cycle
-        := !str_cycle ^ " (" ^ string_of_int !ct ^ ") object " ^ e_str ^ " retaining "
-           ^ MF.monospaced_to_string (e_str ^ "." ^ Typ.Fieldname.to_string f) ^ ", " ;
-        ct := !ct + 1
-    | Sil.Eexp (Exp.Sizeof {typ}, _) ->
-        let step =
-          " (" ^ string_of_int !ct ^ ") an object of "
-          ^ MF.monospaced_to_string (Typ.to_string typ)
-          ^ " retaining another object via instance variable "
-          ^ MF.monospaced_to_string (Typ.Fieldname.to_string f) ^ ", "
-        in
-        str_cycle := !str_cycle ^ step ;
-        ct := !ct + 1
         | _ ->
-        ()
+            Format.sprintf "An object of type %s"
+              (MF.monospaced_to_string (Typ.to_string edge.rc_from.rc_node_typ))
+      in
+      Format.sprintf "(%d) %s retaining another object via instance variable %s, " index
+        from_exp_str
+        (MF.monospaced_to_string (Typ.Fieldname.to_string edge.rc_field.rc_field_name))
+    in
+    let cycle_str = List.mapi ~f:do_edge cycle.rc_elements in
+    String.concat cycle_str ~sep:" "
   in
-  List.iter ~f:do_edge cycle ;
   let desc =
-    Format.sprintf "Retain cycle involving the following objects: %s  %s" !str_cycle
+    Format.sprintf "Retain cycle involving the following objects:%s %s" (desc_retain_cycle cycle)
       (at_line tags loc)
   in
   {no_desc with descriptions= [desc]; tags= !tags; dotty= cycle_dotty}

infer/src/IR/Localise.mli

@@ -201,9 +201,7 @@ val desc_precondition_not_met : pnm_kind option -> Typ.Procname.t -> Location.t
 
 val desc_return_expression_required : string -> Location.t -> error_desc
 
-val desc_retain_cycle :
+val desc_retain_cycle : RetainCyclesType.t -> Location.t -> string option -> error_desc
-  ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> Location.t -> string option
-  -> error_desc
 
 val registered_observer_being_deallocated_str : string -> string
 

infer/src/backend/RetainCycles.ml

@@ -10,64 +10,54 @@ module L = Logging
 module F = Format
 
 let get_cycle root prop =
+  let open RetainCyclesType in
   let sigma = prop.Prop.sigma in
   let get_points_to e =
-    match e with
-    | Sil.Eexp (e', _) ->
     List.find
-          ~f:(fun hpred ->
+      ~f:(fun hpred -> match hpred with Sil.Hpointsto (e', _, _) -> Exp.equal e' e | _ -> false)
-            match hpred with Sil.Hpointsto (e'', _, _) -> Exp.equal e'' e' | _ -> false)
       sigma
-    | _ ->
-        None
-  in
-  let print_cycle cyc =
-    L.d_str "Cycle= " ;
-    List.iter
-      ~f:(fun ((e, t), f, e') ->
-        match (e, e') with
-        | Sil.Eexp (e, _), Sil.Eexp (e', _) ->
-            L.d_str
-              ( "(" ^ Exp.to_string e ^ ": " ^ Typ.to_string t ^ ", " ^ Typ.Fieldname.to_string f
-              ^ ", " ^ Exp.to_string e' ^ ")" )
-        | _ ->
-            ())
-      cyc ;
-    L.d_strln ""
   in
   (* Perform a dfs of a graph stopping when e_root is reached.
-     Returns a pair (path, bool) where path is a list of edges ((e1,type_e1),f,e2)
+   Returns a pair (path, bool) where path is a list of edges 
    describing the path to e_root and bool is true if e_root is reached. *)
-  let rec dfs e_root et_src path el visited =
+  let rec dfs root_node from_node path fields visited =
-    match el with
+    match fields with
     | [] ->
         (path, false)
-    | (f, e) :: el' ->
+    | (field, Sil.Eexp (f_exp, f_inst)) :: el' ->
-        if Sil.equal_strexp e e_root then ((et_src, f, e) :: path, true)
+        if Exp.equal f_exp root_node.rc_node_exp then
-        else if List.mem ~equal:Sil.equal_strexp visited e then (path, false)
+          let rc_field = {rc_field_name= field; rc_field_inst= f_inst} in
+          let edge = {rc_from= from_node; rc_field} in
+          (edge :: path, true)
+        else if List.mem ~equal:Exp.equal visited f_exp then (path, false)
         else
-          let visited' = fst et_src :: visited in
+          let visited' = from_node.rc_node_exp :: visited in
           let res =
-            match get_points_to e with
+            match get_points_to f_exp with
             | None ->
                 (path, false)
-            | Some Sil.Hpointsto (_, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) ->
+            | Some Sil.Hpointsto (_, Sil.Estruct (new_fields, _), Exp.Sizeof {typ= te}) ->
-                dfs e_root (e, te) ((et_src, f, e) :: path) fl visited'
+                let rc_field = {rc_field_name= field; rc_field_inst= f_inst} in
+                let edge = {rc_from= from_node; rc_field} in
+                let rc_to = {rc_node_exp= f_exp; rc_node_typ= te} in
+                dfs root_node rc_to (edge :: path) new_fields visited'
             | _ ->
                 (path, false)
             (* check for lists *)
           in
-          if snd res then res else dfs e_root et_src path el' visited'
+          if snd res then res else dfs root_node from_node path el' visited'
+    | _ ->
+        (path, false)
   in
   L.d_strln "Looking for cycle with root expression: " ;
   Sil.d_hpred root ;
   L.d_strln "" ;
   match root with
   | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) ->
-      let se_root = Sil.Eexp (e_root, Sil.Inone) in
+      let se_root = {rc_node_exp= e_root; rc_node_typ= te} in
       (* start dfs with empty path and expr pointing to root *)
-      let pot_cycle, res = dfs se_root (se_root, te) [] fl [] in
+      let pot_cycle, res = dfs se_root se_root [] fl [] in
-      if res then ( print_cycle pot_cycle ; pot_cycle )
+      if res then pot_cycle
       else (
         L.d_strln "NO cycle found from root" ;
         [] )
@@ -81,45 +71,13 @@ let get_retain_cycle_dotty prop_ cycle =
   | None ->
       None
   | Some Some prop_ ->
-      Dotty.dotty_prop_to_str prop_ cycle
+      Dotty.dotty_retain_cycle_to_str prop_ cycle
   | _ ->
       None
 
 
 let get_var_retain_cycle prop_ =
   let sigma = prop_.Prop.sigma in
-  let is_pvar v h =
-    match h with
-    | Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.equal_strexp v v' ->
-        true
-    | _ ->
-        false
-  in
-  let is_hpred_block v h =
-    match (h, v) with
-    | Sil.Hpointsto (e, _, Exp.Sizeof {typ}), Sil.Eexp (e', _)
-      when Exp.equal e e' && Typ.is_block_type typ ->
-        true
-    | _, _ ->
-        false
-  in
-  let find v = List.find ~f:(is_pvar v) sigma |> Option.map ~f:Sil.hpred_get_lhs in
-  let find_block v =
-    if List.exists ~f:(is_hpred_block v) sigma then Some (Exp.Lvar Sil.block_pvar) else None
-  in
-  let sexp e = Sil.Eexp (e, Sil.Inone) in
-  let find_or_block ((e, t), f, e') =
-    match find e with
-    | Some pvar ->
-        [((sexp pvar, t), f, e')]
-    | _ ->
-      match find_block e with
-      | Some blk ->
-          [((sexp blk, t), f, e')]
-      | _ ->
-          let sizeof = {Exp.typ= t; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in
-          [((sexp (Exp.Sizeof sizeof), t), f, e')]
-  in
   (* returns the pvars of the first cycle we find in sigma.
      This is an heuristic that works if there is one cycle.
      In case there are more than one cycle we may return not necessarily
@@ -130,16 +88,16 @@ let get_var_retain_cycle prop_ =
         []
     | hp :: sigma' ->
         let cycle = get_cycle hp prop_ in
-        L.d_strln "Filtering pvar in cycle " ;
+        if List.is_empty cycle then do_sigma sigma' else cycle
-        let cycle' = List.concat_map ~f:find_or_block cycle in
-        if List.is_empty cycle' then do_sigma sigma' else cycle'
   in
-  do_sigma sigma
+  let cycle_elements = do_sigma sigma in
+  RetainCyclesType.create_cycle cycle_elements
 
 
 (** Checks if cycle has fields (derived from a property or directly defined as ivar) with attributes
     weak/unsafe_unretained/assing *)
 let cycle_has_weak_or_unretained_or_assign_field tenv cycle =
+  let open RetainCyclesType in
   (* returns items annotation for field fn in struct t *)
   let get_item_annotation (t: Typ.t) fn =
     match t.desc with
@@ -171,14 +129,15 @@ let cycle_has_weak_or_unretained_or_assign_field tenv cycle =
     && has_weak_or_unretained_or_assign a.parameters
   in
   let rec do_cycle c =
+    let open RetainCyclesType in
     match c with
     | [] ->
         false
-    | ((_, t), fn, _) :: c' ->
+    | edge :: c' ->
-        let ia = get_item_annotation t fn in
+        let ia = get_item_annotation edge.rc_from.rc_node_typ edge.rc_field.rc_field_name in
         if List.exists ~f:do_annotation ia then true else do_cycle c'
   in
-  do_cycle cycle
+  do_cycle cycle.rc_elements
 
 
 let exn_retain_cycle original_prop hpred cycle =
@@ -192,9 +151,10 @@ let report_cycle tenv hpred original_prop =
         only if it's empty or it has weak or unsafe_unretained fields.
         Otherwise we report a retain cycle. *)
   let remove_opt prop_ = match prop_ with Some Some p -> p | _ -> Prop.prop_emp in
-  let cycle = get_var_retain_cycle (remove_opt original_prop) in
+  match get_var_retain_cycle (remove_opt original_prop) with
-  let ignore_cycle =
+  | Some cycle when not (cycle_has_weak_or_unretained_or_assign_field tenv cycle) ->
-    Int.equal (List.length cycle) 0 || cycle_has_weak_or_unretained_or_assign_field tenv cycle
+      RetainCyclesType.print_cycle cycle ;
-  in
+      Some (exn_retain_cycle original_prop hpred cycle)
-  (ignore_cycle, exn_retain_cycle original_prop hpred cycle)
+  | _ ->
+      None
 

infer/src/backend/RetainCycles.mli

@@ -7,4 +7,4 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  *)
 
-val report_cycle : Tenv.t -> Sil.hpred -> Prop.normal Prop.t option option -> bool * exn
+val report_cycle : Tenv.t -> Sil.hpred -> Prop.normal Prop.t option option -> exn option

infer/src/backend/RetainCyclesType.ml

@@ -0,0 +1,42 @@
+(*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+type retain_cycle_node = {rc_node_exp: Exp.t; rc_node_typ: Typ.t}
+
+type retain_cycle_field_objc = {rc_field_name: Typ.Fieldname.t; rc_field_inst: Sil.inst}
+
+type retain_cycle_edge = {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc}
+
+type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge}
+
+let create_cycle cycle =
+  match cycle with hd :: _ -> Some {rc_elements= cycle; rc_head= hd} | [] -> None
+
+
+let retain_cycle_node_to_string (node: retain_cycle_node) =
+  Format.sprintf "%s : %s" (Exp.to_string node.rc_node_exp) (Typ.to_string node.rc_node_typ)
+
+
+let retain_cycle_field_to_string (field: retain_cycle_field_objc) =
+  Format.sprintf "%s[%s]"
+    (Typ.Fieldname.to_string field.rc_field_name)
+    (Sil.inst_to_string field.rc_field_inst)
+
+
+let retain_cycle_edge_to_string (edge: retain_cycle_edge) =
+  Format.sprintf "%s ->{%s}"
+    (retain_cycle_node_to_string edge.rc_from)
+    (retain_cycle_field_to_string edge.rc_field)
+
+
+let retain_cycle_to_string cycle =
+  "Cycle= \n\t"
+  ^ String.concat ~sep:"->" (List.map ~f:retain_cycle_edge_to_string cycle.rc_elements)
+
+
+let print_cycle cycle = Logging.d_strln (retain_cycle_to_string cycle)

infer/src/backend/RetainCyclesType.mli

@@ -0,0 +1,25 @@
+(*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+type retain_cycle_node = {rc_node_exp: Exp.t; rc_node_typ: Typ.t}
+
+type retain_cycle_field_objc = {rc_field_name: Typ.Fieldname.t; rc_field_inst: Sil.inst}
+
+type retain_cycle_edge = {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc}
+
+(** A retain cycle is a non-empty list of paths. It also contains a pointer to the head of the list 
+to model the cycle structure. The next element from the end of the list is the head. *)
+type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge}
+
+val retain_cycle_to_string : t -> string
+
+val print_cycle : t -> unit
+
+val create_cycle : retain_cycle_edge list -> t option
+(** Creates a cycle if the list is non-empty *)

infer/src/backend/abs.ml

@@ -1131,8 +1131,12 @@ let check_junk ?original_prop pname tenv prop =
               match (alloc_attribute, resource) with
               | Some PredSymb.Awont_leak, Rmemory _ ->
                   (true, exn_leak)
-              | Some _, Rmemory Mobjc when hpred_in_cycle hpred ->
+              | Some _, Rmemory Mobjc when hpred_in_cycle hpred -> (
-                  RetainCycles.report_cycle tenv hpred original_prop
+                match RetainCycles.report_cycle tenv hpred original_prop with
+                | Some exn ->
+                    (false, exn)
+                | None ->
+                    (true, exn_leak) )
               | Some _, Rmemory Mobjc
               | Some _, Rmemory Mnew
               | Some _, Rmemory Mnew_array
@@ -1148,11 +1152,17 @@ let check_junk ?original_prop pname tenv prop =
                   (false, exn_leak)
               | Some _, Rlock ->
                   (false, exn_leak)
-              | _ when hpred_in_cycle hpred && Sil.is_objc_object hpred ->
+              | _ when hpred_in_cycle hpred && Sil.is_objc_object hpred -> (
+                match
                   (* When it's a cycle and it is an Objective-C object then
                         we have a retain cycle. Objc object may not have the
                         Mobjc qualifier when added in footprint doing abduction *)
                   RetainCycles.report_cycle tenv hpred original_prop
+                with
+                | Some exn ->
+                    (false, exn)
+                | None ->
+                    (true, exn_leak) )
               | _ ->
                   (Config.curr_language_is Config.Java, exn_leak)
             in

infer/src/backend/dotty.ml

@@ -1097,8 +1097,24 @@ let pp_dotty_prop fmt (prop, cycle) =
   Format.fprintf fmt "@\n}"
 
 
-let dotty_prop_to_str prop cycle =
+let dotty_retain_cycle_to_str prop (cycle: RetainCyclesType.t) =
-  try Some (F.asprintf "%a" pp_dotty_prop (prop, cycle))
+  let open RetainCyclesType in
+  let rec cycle_to_list elements =
+    match elements with
+    | edge1 :: edge2 :: rest ->
+        ( edge1.rc_from.rc_node_exp
+        , edge1.rc_field.rc_field_name
+        , Sil.Eexp (edge2.rc_from.rc_node_exp, Sil.Inone) )
+        :: cycle_to_list (edge2 :: rest)
+    | [edge] ->
+        [ ( edge.rc_from.rc_node_exp
+          , edge.rc_field.rc_field_name
+          , Sil.Eexp (cycle.rc_head.rc_from.rc_node_exp, Sil.Inone) ) ]
+    | [] ->
+        []
+  in
+  let cycle_list = cycle_to_list cycle.rc_elements in
+  try Some (F.asprintf "%a" pp_dotty_prop (prop, cycle_list))
   with exn when SymOp.exn_not_failure exn -> None
 
 
@@ -1717,3 +1733,4 @@ let print_specs_xml signature specs loc fmt =
       [xml_signature; xml_specifications]
   in
   Io_infer.Xml.pp_document true fmt proc_summary
+

infer/src/backend/dotty.mli

@@ -49,8 +49,7 @@ val dotty_prop_to_dotty_file :
   string -> Prop.normal Prop.t -> ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list
   -> unit
 
-val dotty_prop_to_str :
+val dotty_retain_cycle_to_str : Prop.normal Prop.t -> RetainCyclesType.t -> string option
-  Prop.normal Prop.t -> ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> string option
 
 val reset_node_counter : unit -> unit
 (** reset the counter used for node and heap identifiers *)

infer/src/backend/errdesc.mli

@@ -101,9 +101,7 @@ val explain_frontend_warning : string -> string option -> Location.t -> Localise
 val explain_return_statement_missing : Location.t -> Localise.error_desc
 (** explain a return statement missing *)
 
-val explain_retain_cycle :
+val explain_retain_cycle : RetainCyclesType.t -> Location.t -> string option -> Localise.error_desc
-  ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> Location.t -> string option
-  -> Localise.error_desc
 (** explain a retain cycle *)
 
 val explain_unary_minus_applied_to_unsigned_expression :