[retain cycles] Do not check twice for cycles, once in abs and once in the retain cycles module

Reviewed By: ddino

Differential Revision: D6723385

fbshipit-source-id: 5fe64b4

infer/src/backend/RetainCycles.ml

@@ -100,21 +100,12 @@ let get_cycle root prop =
       []
 
 
-let get_var_retain_cycle prop_ =
-  let sigma = prop_.Prop.sigma in
+let get_var_retain_cycle hpred prop_ =
   (* 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
      the one we are looking for. *)
-  let rec do_sigma sigma_todo =
-    match sigma_todo with
-    | [] ->
-        []
-    | hp :: sigma' ->
-        let cycle = get_cycle hp prop_ in
-        if List.is_empty cycle then do_sigma sigma' else cycle
-  in
-  let cycle_elements = do_sigma sigma in
+  let cycle_elements = get_cycle hpred prop_ in
   RetainCyclesType.create_cycle cycle_elements
 
 
@@ -177,7 +168,7 @@ let report_cycle tenv hpred original_prop =
         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 prop with
+  match get_var_retain_cycle hpred prop with
   | Some cycle when not (cycle_has_weak_or_unretained_or_assign_field tenv cycle) ->
       RetainCyclesType.print_cycle cycle ;
       Some (exn_retain_cycle tenv prop hpred cycle)

infer/src/backend/RetainCyclesType.ml

@@ -8,25 +8,30 @@
  *)
 open! IStd
 
-type retain_cycle_node = {rc_node_exp: Exp.t; rc_node_typ: Typ.t}
+type retain_cycle_node = {rc_node_exp: Exp.t; rc_node_typ: Typ.t} [@@deriving compare]
 
-type retain_cycle_field_objc = {rc_field_name: Typ.Fieldname.t; rc_field_inst: Sil.inst}
+type retain_cycle_field_objc =
+  {rc_field_name: Typ.Fieldname.t; rc_field_inst: Sil.inst}
+  [@@deriving compare]
 
-type retain_cycle_edge = {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc}
+type retain_cycle_edge =
+  {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc}
+  [@@deriving compare]
 
-type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge}
+type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge} [@@deriving compare]
 
 let create_cycle cycle =
-  match cycle with
+  let sorted_cycle = List.sort ~cmp:compare_retain_cycle_edge cycle in
+  match sorted_cycle with
   | [hd] -> (
     match (* cycles of length 1 created at rearrange are not real *)
           hd.rc_field.rc_field_inst with
     | Sil.Irearrange _ ->
         None
     | _ ->
-        Some {rc_elements= cycle; rc_head= hd} )
+        Some {rc_elements= sorted_cycle; rc_head= hd} )
   | hd :: _ ->
-      Some {rc_elements= cycle; rc_head= hd}
+      Some {rc_elements= sorted_cycle; rc_head= hd}
   | [] ->
       None
 

infer/src/backend/abs.ml

@@ -1034,28 +1034,6 @@ let check_junk ?original_prop pname tenv prop =
       in
       List.for_all ~f:predicate entries
     in
-    let hpred_in_cycle hpred =
-      (* check if the predicate belongs to a cycle in the heap *)
-      let id_in_cycle id =
-        let set1 = sigma_reachable (Sil.fav_from_list [id]) sigma in
-        let set2 = Ident.IdentSet.remove id set1 in
-        let fav2 = Sil.fav_from_list (Ident.IdentSet.elements set2) in
-        let set3 = sigma_reachable fav2 sigma in
-        Ident.IdentSet.mem id set3
-      in
-      let entries = Sil.hpred_entries hpred in
-      let predicate = function Exp.Var id -> id_in_cycle id | _ -> false in
-      let hpred_is_loop =
-        match hpred with
-        (* true if hpred has a self loop, ie one field points to id *)
-        | Sil.Hpointsto (Exp.Var id, se, _) ->
-            let fav = Sil.fav_new () in
-            Sil.strexp_fav_add fav se ; Sil.fav_mem fav id
-        | _ ->
-            false
-      in
-      hpred_is_loop || List.exists ~f:predicate entries
-    in
     let rec remove_junk_recursive sigma_done sigma_todo =
       match sigma_todo with
       | [] ->
@@ -1130,13 +1108,13 @@ 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 -> (
                 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)
+              | (Some _, Rmemory Mnew | Some _, Rmemory Mnew_array)
                 when Config.curr_language_is Config.Clang ->
                   (is_none ml_bucket_opt, exn_leak)
               | Some _, Rmemory _ ->
@@ -1149,7 +1127,7 @@ 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 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
@@ -1159,7 +1137,7 @@ let check_junk ?original_prop pname tenv prop =
                 | Some exn ->
                     (false, exn)
                 | None ->
-                    (true, exn_leak) )
+                    (Config.curr_language_is Config.Java, exn_leak) )
               | _ ->
                   (Config.curr_language_is Config.Java, exn_leak)
             in