[retain cycles] Implement dotty files for retain cycles new

Reviewed By: mbouaziz

Differential Revision: D6925776

fbshipit-source-id: 235f010

infer/src/backend/RetainCycles.ml

@@ -32,7 +32,7 @@ let desc_retain_cycle tenv (cycle: RetainCyclesType.t) =
           in
           if List.is_empty update_str_list then " "
           else ", " ^ String.concat ~sep:"," update_str_list
-      | Block ->
+      | Block _ ->
           ""
     in
     let cycle_item_str =
@@ -41,7 +41,7 @@ let desc_retain_cycle tenv (cycle: RetainCyclesType.t) =
           MF.monospaced_to_string
             (Format.sprintf "%s->%s" (from_exp_str obj)
                (Typ.Fieldname.to_string obj.rc_field.rc_field_name))
-      | Block ->
+      | Block _ ->
           Format.sprintf "a block"
     in
     Format.sprintf "(%d) %s%s" index cycle_item_str location_str
@@ -59,14 +59,12 @@ let get_cycle root prop =
       sigma
   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 
+   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 root_node from_node path fields visited =
     let get_cycle_blocks exp =
       match exp with
-      | Exp.Closure {captured_vars}
+      | Exp.Closure {name; captured_vars} ->
-      (* will turn on in prod when false positives have been addressed *)
-        when Config.debug_exceptions ->
           List.find
             ~f:(fun (e, _, typ) ->
               match typ.Typ.desc with
@@ -75,7 +73,7 @@ let get_cycle root prop =
               | _ ->
                   Exp.equal e root_node.rc_node_exp )
             captured_vars
-          |> Option.map ~f:snd3
+          |> Option.map ~f:(fun (_, var, _) -> (name, var))
       | _ ->
           None
     in
@@ -91,13 +89,13 @@ let get_cycle root prop =
           let cycle_block_opt = get_cycle_blocks f_exp in
           if Option.is_some cycle_block_opt then
             match cycle_block_opt with
-            | Some var ->
+            | Some (procname, var) ->
                 let rc_field = {rc_field_name= field; rc_field_inst= f_inst} in
-                (* From the captured variables we get the actual name of the variable 
+                (* From the captured variables we get the actual name of the variable
                 that is more useful for the error message *)
                 let updated_from_node = {from_node with rc_node_exp= Exp.Lvar var} in
                 let edge1 = Object {rc_from= updated_from_node; rc_field} in
-                let edge2 = Block in
+                let edge2 = Block procname in
                 (edge1 :: edge2 :: path, true)
             | None ->
                 assert false
@@ -191,16 +189,21 @@ let cycle_has_weak_or_unretained_or_assign_field tenv cycle =
       | Object obj ->
           let ia = get_item_annotation obj.rc_from.rc_node_typ obj.rc_field.rc_field_name in
           if List.exists ~f:do_annotation ia then true else do_cycle c'
-      | Block ->
+      | Block _ ->
           false
   in
   do_cycle cycle.rc_elements
 
 
-let exn_retain_cycle tenv prop hpred cycle =
+let exn_retain_cycle tenv hpred cycle =
   let retain_cycle = desc_retain_cycle tenv cycle in
-  let cycle_dotty = Dotty.dotty_retain_cycle_to_str prop cycle in
+  let cycle_dotty = Format.asprintf "%a" RetainCyclesType.pp_dotty cycle in
-  let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) cycle_dotty in
+  ( if Config.debug_mode then
+      let rc_dotty_dir = Filename.concat Config.results_dir Config.retain_cycle_dotty_dir in
+      Utils.create_dir rc_dotty_dir ;
+      let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in
+      RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ;
+  let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) (Some cycle_dotty) in
   Exceptions.Retain_cycle (hpred, desc, __POS__)
 
 
@@ -213,6 +216,6 @@ let report_cycle tenv hpred original_prop =
   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)
+      Some (exn_retain_cycle tenv hpred cycle)
   | _ ->
       None

infer/src/backend/RetainCyclesType.ml

@@ -18,7 +18,10 @@ type retain_cycle_edge_objc =
   {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc}
   [@@deriving compare]
 
-type retain_cycle_edge = Object of retain_cycle_edge_objc | Block [@@deriving compare]
+type retain_cycle_edge =
+  | Object of retain_cycle_edge_objc
+  | Block of Typ.Procname.t
+  [@@deriving compare]
 
 type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge} [@@deriving compare]
 
@@ -26,7 +29,7 @@ let is_inst_rearrange node =
   match node with
   | Object obj -> (
     match obj.rc_field.rc_field_inst with Sil.Irearrange _ -> true | _ -> false )
-  | Block ->
+  | Block _ ->
       false
 
 
@@ -59,7 +62,7 @@ let retain_cycle_edge_to_string (edge: retain_cycle_edge) =
       Format.sprintf "%s ->{%s}"
         (retain_cycle_node_to_string obj.rc_from)
         (retain_cycle_field_to_string obj.rc_field)
-  | Block ->
+  | Block _ ->
       Format.sprintf "a block"
 
 
@@ -69,3 +72,54 @@ let retain_cycle_to_string cycle =
 
 
 let print_cycle cycle = Logging.d_strln (retain_cycle_to_string cycle)
+
+let pp_dotty fmt cycle =
+  let pp_dotty_obj fmt element =
+    match element with
+    | Object obj ->
+        Format.fprintf fmt "Object: %a" (Typ.pp Pp.text) obj.rc_from.rc_node_typ
+    | Block _ ->
+        Format.fprintf fmt "Block"
+  in
+  let pp_dotty_id fmt element =
+    match element with
+    | Object obj ->
+        Typ.pp Pp.text fmt obj.rc_from.rc_node_typ
+    | Block name ->
+        Format.fprintf fmt "%s" (Typ.Procname.to_unique_id name)
+  in
+  let pp_dotty_field fmt element =
+    match element with
+    | Object obj ->
+        Typ.Fieldname.pp fmt obj.rc_field.rc_field_name
+    | Block _ ->
+        Format.fprintf fmt ""
+  in
+  let pp_dotty_element fmt element =
+    Format.fprintf fmt "\t%a [label = \"%a | %a \"]@\n" pp_dotty_id element pp_dotty_obj element
+      pp_dotty_field element
+  in
+  let rec pp_dotty_edges fmt edges =
+    match edges with
+    | edge1 :: edge2 :: rest ->
+        Format.fprintf fmt "\t%a -> %a [color=\"blue\"];@\n" pp_dotty_id edge1 pp_dotty_id edge2 ;
+        pp_dotty_edges fmt (edge2 :: rest)
+    | [edge] ->
+        Format.fprintf fmt "\t%a -> %a [color=\"blue\"];@\n" pp_dotty_id edge pp_dotty_id
+          cycle.rc_head
+    | [] ->
+        ()
+  in
+  Format.fprintf fmt "@\n@\n@\ndigraph main { @\n\tnode [shape=record]; @\n" ;
+  Format.fprintf fmt "@\n\trankdir =LR; @\n" ;
+  Format.fprintf fmt "@\n" ;
+  List.iter ~f:(pp_dotty_element fmt) cycle.rc_elements ;
+  Format.fprintf fmt "@\n" ;
+  pp_dotty_edges fmt cycle.rc_elements ;
+  Format.fprintf fmt "@\n}"
+
+
+let write_dotty_to_file fname cycle =
+  let chan = Out_channel.create fname in
+  let fmt = Format.formatter_of_out_channel chan in
+  pp_dotty fmt cycle ; Out_channel.close chan

infer/src/backend/RetainCyclesType.mli

@@ -15,9 +15,9 @@ type retain_cycle_field_objc = {rc_field_name: Typ.Fieldname.t; rc_field_inst: S
 
 type retain_cycle_edge_objc = {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc}
 
-type retain_cycle_edge = Object of retain_cycle_edge_objc | Block
+type retain_cycle_edge = Object of retain_cycle_edge_objc | Block of Typ.Procname.t
 
-(** A retain cycle is a non-empty list of paths. It also contains a pointer to the head of the list 
+(** 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}
 
@@ -25,3 +25,7 @@ val print_cycle : t -> unit
 
 val create_cycle : retain_cycle_edge list -> t option
 (** Creates a cycle if the list is non-empty *)
+
+val pp_dotty : Format.formatter -> t -> unit
+
+val write_dotty_to_file : string -> t -> unit

infer/src/backend/dotty.ml

@@ -19,7 +19,6 @@ module F = Format
 let print_full_prop = ref false
 
 type kind_of_dotty_prop =
-  | Generic_proposition
   | Spec_precondition
   | Spec_postcondition of Prop.normal Prop.t  (** the precondition associated with the post *)
   | Lambda_pred of int * int * bool
@@ -712,10 +711,6 @@ let print_kind f kind =
       F.fprintf f "@\n POST%iL0 [label=\"POST %i \",  style=filled, color= yellow]@\n"
         !dotty_state_count !post_counter ;
       print_stack_info := true
-  | Generic_proposition ->
-      if !print_full_prop then
-        F.fprintf f "@\n HEAP%iL0 [label=\"HEAP %i \",  style=filled, color= yellow]@\n"
-          !dotty_state_count !proposition_counter
   | Lambda_pred (no, lev, array) ->
     match array with
     | false ->
@@ -1071,50 +1066,6 @@ let pp_dotty_one_spec f pre posts =
   F.fprintf f "@\n } @\n"
 
 
-let pp_dotty_prop fmt (prop, cycle) =
-  reset_proposition_counter () ;
-  Format.fprintf fmt "@\n@\n@\ndigraph main { @\nnode [shape=box]; @\n" ;
-  Format.fprintf fmt "@\n compound = true; rankdir =LR; @\n" ;
-  pp_dotty fmt Generic_proposition prop (Some cycle) ;
-  Format.fprintf fmt "@\n}"
-
-
-let dotty_retain_cycle_to_str prop (cycle: RetainCyclesType.t) =
-  let open RetainCyclesType in
-  let get_exp_from_edge edge =
-    match edge with
-    | Object obj ->
-        obj.rc_from.rc_node_exp
-    | Block ->
-        Exp.Lvar (Pvar.mk (Mangled.from_string "block") (Typ.Procname.from_string_c_fun ""))
-  in
-  let get_field_from_edge edge =
-    match edge with
-    | Object obj ->
-        obj.rc_field.rc_field_name
-    | Block ->
-        Typ.Fieldname.Java.from_string ""
-  in
-  let open RetainCyclesType in
-  let rec cycle_to_list elements =
-    match elements with
-    | edge1 :: edge2 :: rest ->
-        ( get_exp_from_edge edge1
-        , get_field_from_edge edge1
-        , Sil.Eexp (get_exp_from_edge edge2, Sil.Inone) )
-        :: cycle_to_list (edge2 :: rest)
-    | [edge] ->
-        [ ( get_exp_from_edge edge
-          , get_field_from_edge edge
-          , Sil.Eexp (get_exp_from_edge edge, 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
-
-
 (********** START of Print interprocedural cfgs in dotty format  *)
 (********** Print control flow graph (in dot form) for fundec to channel. You have to compute an
             interprocedural cfg first. *)

infer/src/backend/dotty.mli

@@ -21,5 +21,3 @@ val print_icfg_dotty : SourceFile.t -> Cfg.t -> unit
 
 val pp_speclist_dotty_file : DB.filename -> Prop.normal Specs.spec list -> unit
 (** Dotty printing for specs *)
-
-val dotty_retain_cycle_to_str : Prop.normal Prop.t -> RetainCyclesType.t -> string option

infer/src/base/Config.ml

@@ -275,6 +275,8 @@ let report_nullable_inconsistency = true
 
 let reporting_stats_dir_name = "reporting_stats"
 
+let retain_cycle_dotty_dir = "retain_cycle_dotty"
+
 (** If true, compact summaries before saving *)
 let save_compact_summaries = true
 

infer/src/base/Config.mli

@@ -195,6 +195,8 @@ val report_nullable_inconsistency : bool
 
 val reporting_stats_dir_name : string
 
+val retain_cycle_dotty_dir : string
+
 val save_compact_summaries : bool
 
 val smt_output : bool

infer/tests/codetoanalyze/objc/errors/Makefile

@@ -28,6 +28,7 @@ SOURCES_DEFAULT = \
 	memory_leaks_benchmark/NSData_models_tests.m \
   memory_leaks_benchmark/RetainReleaseExampleBucketing.m \
 	memory_leaks_benchmark/CoreVideoExample.m \
+	memory_leaks_benchmark/RetainCycleLength3.m \
   npe/Fraction.m \
   npe/NPD_core_foundation.m \
   npe/Npe_with_equal_names.m \

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

@@ -70,6 +70,7 @@ codetoanalyze/objc/errors/variadic_methods/premature_nil_termination.m, Prematur
 codetoanalyze/objc/errors/memory_leaks_benchmark/CoreVideoExample.m, CoreVideoExample_cvpixelbuffer_not_released_leak, 1, MEMORY_LEAK, [start of procedure cvpixelbuffer_not_released_leak]
 codetoanalyze/objc/errors/memory_leaks_benchmark/NSData_models_tests.m, NSData_models_tests_macForIV:, 2, MEMORY_LEAK, [start of procedure macForIV:]
 codetoanalyze/objc/errors/memory_leaks_benchmark/NSString_models_tests.m, StringInitA_hexStringValue, 11, MEMORY_LEAK, [start of procedure hexStringValue,Skipping CFStringCreateWithBytesNoCopy(): function or method not found,Condition is false]
+codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleLength3.m, strongcycle, 6, RETAIN_CYCLE, [start of procedure strongcycle()]
 codetoanalyze/objc/errors/npe/Fraction.m, test_virtual_call, 7, NULL_DEREFERENCE, [start of procedure test_virtual_call(),start of procedure setNumerator:,return from a call to Fraction_setNumerator:,start of procedure getNumerator,return from a call to Fraction_getNumerator,Condition is true]
 codetoanalyze/objc/errors/npe/Npe_with_equal_names.m, EqualNamesTest, 3, NULL_DEREFERENCE, [start of procedure EqualNamesTest(),start of procedure meth,return from a call to EqualNamesA_meth]
 codetoanalyze/objc/errors/npe/block.m, BlockA_doSomethingThenCallback:, 2, PARAMETER_NOT_NULL_CHECKED, [start of procedure doSomethingThenCallback:]

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

@@ -0,0 +1,48 @@
+/*
+ * Copyright (c) 2013 - 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.
+ */
+
+#import <Foundation/NSObject.h>
+
+@class AA;
+@class BB;
+@class CC;
+
+@interface AA : NSObject
+
+@property(nonatomic, strong) BB* b;
+@end
+
+@implementation AA
+@end
+
+@interface BB : NSObject
+
+@property(nonatomic, strong) CC* c;
+@end
+
+@implementation BB
+@end
+
+@interface CC : NSObject
+
+@property(nonatomic, strong) AA* a;
+@end
+
+@implementation CC
+@end
+
+int strongcycle() {
+  AA* a_obj = [AA new];
+  BB* b_obj = [BB new];
+  CC* c_obj = [CC new];
+  a_obj.b = b_obj;
+  b_obj.c = c_obj;
+  c_obj.a = a_obj; // Retain cycle
+  return 0;
+}