[retain cycles] Find all the cycles available instead of only one per root analysed

Reviewed By: mbouaziz

Differential Revision: D7042007

fbshipit-source-id: 96c7686

infer/src/backend/RetainCycles.ml

@@ -88,6 +88,18 @@ let edge_is_strong tenv obj_edge =
   not weak_edge
 
 
+exception Max_retain_cycles of RetainCyclesType.Set.t
+
+let add_cycle found_cycles rev_path =
+  match RetainCyclesType.create_cycle (List.rev rev_path) with
+  | Some cycle ->
+      if RetainCyclesType.Set.cardinal found_cycles < 10 then
+        RetainCyclesType.Set.add cycle found_cycles
+      else raise (Max_retain_cycles found_cycles)
+  | None ->
+      found_cycles
+
+
 let get_cycle_blocks root_node exp =
   match exp with
   | Exp.Closure {name; captured_vars} ->
@@ -105,7 +117,7 @@ let get_cycle_blocks root_node exp =
       None
 
 
-let get_cycle root tenv prop =
+let get_cycles found_cycles root tenv prop =
   let open RetainCyclesType in
   let sigma = prop.Prop.sigma in
   let get_points_to e =
@@ -113,46 +125,45 @@ let get_cycle root tenv prop =
       ~f:(fun hpred -> match hpred with Sil.Hpointsto (e', _, _) -> Exp.equal e' e | _ -> false)
       sigma
   in
-  (* Perform a dfs of a graph stopping when e_root is reached.
+  (* Perform a dfs of a graph stopping when e_root is reached. Returns the set of cycles reached. *)
-   Returns a pair (path, bool) where path is a list of edges
+  let rec dfs ~found_cycles ~root_node ~from_node ~rev_path ~fields ~visited =
-   describing the path to e_root and bool is true if e_root is reached. *)
-  let rec dfs ~root_node ~from_node ~rev_path ~fields ~visited =
     match fields with
     | [] ->
-        (rev_path, false)
+        found_cycles
     | (field, Sil.Eexp (f_exp, f_inst)) :: el' ->
         let rc_field = {rc_field_name= field; rc_field_inst= f_inst} in
         let obj_edge = {rc_from= from_node; rc_field} in
         let edge = Object obj_edge in
-        (* found root, finish the cycle *)
+        let visited' = from_node.rc_node_exp :: visited in
-        if edge_is_strong tenv obj_edge && Exp.equal f_exp root_node.rc_node_exp then
+        let found_cycles' =
-          (edge :: rev_path, true) (* we already visited f_exp, stop *)
+          (* found root, finish the cycle *)
-        else if List.mem ~equal:Exp.equal visited f_exp then (rev_path, false)
+          if edge_is_strong tenv obj_edge && Exp.equal f_exp root_node.rc_node_exp then
-        else
+            add_cycle found_cycles (edge :: rev_path) (* we already visited f_exp, stop *)
-          let visited' = from_node.rc_node_exp :: visited in
+          else if List.mem ~equal:Exp.equal visited f_exp then found_cycles
-          let cycle_block_opt = get_cycle_blocks root_node f_exp in
-          (* cycle with a block *)
-          if edge_is_strong tenv obj_edge && Option.is_some cycle_block_opt then
-            let procname = Option.value_exn cycle_block_opt in
-            let edge2 = Block procname in
-            (edge2 :: edge :: rev_path, true)
           else
-            let res =
+            (* cycle with a block *)
+            let cycle_opt = get_cycle_blocks root_node f_exp in
+            if edge_is_strong tenv obj_edge && Option.is_some cycle_opt then
+              let procname = Option.value_exn cycle_opt in
+              let edge2 = Block procname in
+              let rev_path' = edge2 :: edge :: rev_path in
+              add_cycle found_cycles rev_path'
+            else
               match get_points_to f_exp with
               | None ->
-                  (rev_path, false)
+                  found_cycles
               | Some Sil.Hpointsto (_, Sil.Estruct (new_fields, _), Exp.Sizeof {typ= te})
                 when edge_is_strong tenv obj_edge ->
                   let rc_to = {rc_node_exp= f_exp; rc_node_typ= te} in
-                  dfs ~root_node ~from_node:rc_to ~rev_path:(edge :: rev_path) ~fields:new_fields
+                  dfs ~found_cycles ~root_node ~from_node:rc_to ~rev_path:(edge :: rev_path)
-                    ~visited:visited'
+                    ~fields:new_fields ~visited:visited'
               | _ ->
-                  (rev_path, false)
+                  found_cycles
-            in
+        in
-            if snd res then res
+        dfs ~found_cycles:found_cycles' ~root_node ~from_node ~rev_path ~fields:el'
-            else dfs ~root_node ~from_node ~rev_path ~fields:el' ~visited:visited'
+          ~visited:visited'
     | _ ->
-        (rev_path, false)
+        found_cycles
   in
   L.d_strln "Looking for cycle with root expression: " ;
   Sil.d_hpred root ;
@@ -161,25 +172,16 @@ let get_cycle root tenv prop =
   | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) ->
       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 ~found_cycles ~root_node:se_root ~from_node:se_root ~rev_path:[] ~fields:fl ~visited:[]
-        dfs ~root_node:se_root ~from_node:se_root ~rev_path:[] ~fields:fl ~visited:[]
-      in
-      if res then List.rev pot_cycle
-      else (
-        L.d_strln "NO cycle found from root" ;
-        [] )
   | _ ->
       L.d_strln "Root exp is not an allocated object. No cycle found" ;
-      []
+      found_cycles
 
 
-let get_var_retain_cycle hpred tenv prop_ =
+(* Find all the cycles available with root hpred, up to a limit of 10 *)
-  (* returns the pvars of the first cycle we find in sigma.
+let get_retain_cycles hpred tenv prop_ =
-     This is an heuristic that works if there is one cycle.
+  try get_cycles RetainCyclesType.Set.empty hpred tenv prop_ with Max_retain_cycles cycles ->
-     In case there are more than one cycle we may return not necessarily
+    cycles
-     the one we are looking for. *)
-  let cycle_elements = get_cycle hpred tenv prop_ in
-  RetainCyclesType.create_cycle cycle_elements
 
 
 let exn_retain_cycle tenv hpred cycle =
@@ -194,15 +196,20 @@ let exn_retain_cycle tenv hpred cycle =
   Exceptions.Retain_cycle (hpred, desc, __POS__)
 
 
-let report_cycle tenv hpred original_prop =
+let report_cycle tenv pname hpred original_prop =
   (* When there is a cycle in objc we ignore it
         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 prop = remove_opt original_prop in
-  match get_var_retain_cycle hpred tenv prop with
+  let cycles = get_retain_cycles hpred tenv prop in
-  | Some cycle ->
+  RetainCyclesType.Set.iter RetainCyclesType.print_cycle cycles ;
-      RetainCyclesType.print_cycle cycle ;
+  match Specs.get_summary pname with
-      Some (exn_retain_cycle tenv hpred cycle)
+  | Some summary ->
-  | _ ->
+      RetainCyclesType.Set.iter
-      None
+        (fun cycle ->
+          let exn = exn_retain_cycle tenv hpred cycle in
+          Reporting.log_error summary exn )
+        cycles
+  | None ->
+      ()

infer/src/backend/RetainCycles.mli

@@ -9,4 +9,5 @@
 
 open! IStd
 
-val report_cycle : Tenv.t -> Sil.hpred -> Prop.normal Prop.t option option -> exn option
+val report_cycle :
+  Tenv.t -> Typ.Procname.t -> Sil.hpred -> Prop.normal Prop.t option option -> unit

infer/src/backend/RetainCyclesType.ml

@@ -25,7 +25,13 @@ type retain_cycle_edge =
 
 let retain_cycle_edge_equal = [%compare.equal : retain_cycle_edge]
 
-type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge} [@@deriving compare]
+type t = {rc_head: retain_cycle_edge; rc_elements: retain_cycle_edge list} [@@deriving compare]
+
+module Set = Caml.Set.Make (struct
+  type nonrec t = t
+
+  let compare = compare
+end)
 
 let is_inst_rearrange node =
   match node with
@@ -55,12 +61,12 @@ let _retain_cycle_edge_to_string (edge: retain_cycle_edge) =
       Format.sprintf "a block"
 
 
-let retain_cycle_to_string cycle =
+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)
+let print_cycle cycle = Logging.d_strln (_retain_cycle_to_string cycle)
 
 let find_minimum_element cycle =
   List.reduce_exn cycle.rc_elements ~f:(fun el1 el2 ->

infer/src/backend/RetainCyclesType.mli

@@ -19,7 +19,10 @@ type retain_cycle_edge = Object of retain_cycle_edge_objc | Block of Typ.Procnam
 
 (** 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}
+type t = {rc_head: retain_cycle_edge; rc_elements: retain_cycle_edge list}
+
+(** Set for retain cycles. *)
+module Set : Caml.Set.S with type elt = t
 
 val print_cycle : t -> unit
 
@@ -33,3 +36,5 @@ val write_dotty_to_file : string -> t -> unit
 val _retain_cycle_edge_to_string : retain_cycle_edge -> string
 
 val _retain_cycle_node_to_string : retain_cycle_node -> string
+
+val _retain_cycle_to_string : t -> string

infer/src/backend/abs.ml

@@ -1107,12 +1107,10 @@ let check_junk ?original_prop pname tenv prop =
               match (alloc_attribute, resource) with
               | Some PredSymb.Awont_leak, Rmemory _ ->
                   (true, exn_leak)
-              | Some _, Rmemory Mobjc -> (
+              | Some _, Rmemory Mobjc ->
-                match RetainCycles.report_cycle tenv hpred original_prop with
+                  RetainCycles.report_cycle tenv pname hpred original_prop ;
-                | Some exn ->
+                  (true, exn_leak)
-                    (false, exn)
+                  (* we report now inside RetainCycles, here we ignore the leak *)
-                | None ->
-                    (true, exn_leak) )
               | (Some _, Rmemory Mnew | Some _, Rmemory Mnew_array)
                 when Language.curr_language_is Clang ->
                   (is_none ml_bucket_opt, exn_leak)
@@ -1126,17 +1124,13 @@ let check_junk ?original_prop pname tenv prop =
                   (false, exn_leak)
               | Some _, Rlock ->
                   (false, exn_leak)
-              | _ when Sil.is_objc_object hpred -> (
+              | _ when 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
+                  RetainCycles.report_cycle tenv pname hpred original_prop ;
-                with
+                  (true, exn_leak)
-                | Some exn ->
+                  (* we report now inside RetainCycles, here we ignore the leak *)
-                    (false, exn)
-                | None ->
-                    (Language.curr_language_is Java, exn_leak) )
               | _ ->
                   (Language.curr_language_is Java, exn_leak)
             in

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -30,7 +30,8 @@ codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, field_set_correc
 codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, implicit_expr_set_correctly, 3, DIVIDE_BY_ZERO, [start of procedure implicit_expr_set_correctly()]
 codetoanalyze/objc/errors/initialization/struct_initlistexpr.c, point_coords_set_correctly, 2, DIVIDE_BY_ZERO, [start of procedure point_coords_set_correctly()]
 codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, call_retain_self_in_block_cycle, 2, RETAIN_CYCLE, [start of procedure call_retain_self_in_block_cycle(),start of procedure retain_self_in_block,return from a call to RCBlock_retain_self_in_block]
-codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 4, RETAIN_CYCLE, [start of procedure retain_a_in_block_cycle()]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 5, RETAIN_CYCLE, [start of procedure retain_a_in_block_cycle()]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m, retain_a_in_block_cycle, 5, RETAIN_CYCLE, [start of procedure retain_a_in_block_cycle()]
 codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle.m, strongcycle, 6, RETAIN_CYCLE, [start of procedure strongcycle()]
 codetoanalyze/objc/errors/memory_leaks_benchmark/retain_cycle2.m, strongcycle2, 4, RETAIN_CYCLE, [start of procedure strongcycle2(),start of procedure init,return from a call to Parent_init,start of procedure init,return from a call to Child_init,start of procedure setChild:,return from a call to Parent_setChild:,start of procedure setParent:,return from a call to Child_setParent:]
 codetoanalyze/objc/errors/npe/UpdateDict.m, add_nil_in_dict, 10, NULL_DEREFERENCE, [start of procedure add_nil_in_dict(),Skipping dictionaryWithObjectsAndKeys:: function or method not found]

infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleBlocks.m

@@ -26,6 +26,8 @@ typedef void (^MyAHandler)(RCBlockAA* name);
   RCBlock* child;
 }
 
+@property(nonatomic, strong) RCBlockAA* a;
+
 @property(nonatomic, strong) MyHandler handler;
 
 @property(nonatomic, strong) MyAHandler a_handler;
@@ -78,6 +80,7 @@ int retain_a_in_block_cycle() {
   RCBlockAA* a = [RCBlockAA new];
   RCBlock* b = [RCBlock new];
   a.b = b;
+  b.a = a;
   b.a_handler = ^(RCBlockAA* b) {
     a.child = a;
   };