From 4218142a84a8592b5bd0b305ff5375e588762f61 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Thu, 8 Feb 2018 06:15:27 -0800 Subject: [PATCH] [retain cycles] Implement dotty files for retain cycles new Reviewed By: mbouaziz Differential Revision: D6925776 fbshipit-source-id: 235f010 --- infer/src/backend/RetainCycles.ml | 33 +++++----- infer/src/backend/RetainCyclesType.ml | 60 ++++++++++++++++++- infer/src/backend/RetainCyclesType.mli | 8 ++- infer/src/backend/dotty.ml | 49 --------------- infer/src/backend/dotty.mli | 2 - infer/src/base/Config.ml | 2 + infer/src/base/Config.mli | 2 + .../tests/codetoanalyze/objc/errors/Makefile | 1 + .../codetoanalyze/objc/errors/issues.exp | 1 + .../RetainCycleLength3.m | 48 +++++++++++++++ 10 files changed, 135 insertions(+), 71 deletions(-) create mode 100644 infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleLength3.m diff --git a/infer/src/backend/RetainCycles.ml b/infer/src/backend/RetainCycles.ml index fa2ab60ab..aa0e526dc 100644 --- a/infer/src/backend/RetainCycles.ml +++ b/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} - (* will turn on in prod when false positives have been addressed *) - when Config.debug_exceptions -> + | Exp.Closure {name; captured_vars} -> 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 desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) cycle_dotty in + let cycle_dotty = Format.asprintf "%a" RetainCyclesType.pp_dotty cycle 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 diff --git a/infer/src/backend/RetainCyclesType.ml b/infer/src/backend/RetainCyclesType.ml index 167e7d06b..ab439b471 100644 --- a/infer/src/backend/RetainCyclesType.ml +++ b/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 diff --git a/infer/src/backend/RetainCyclesType.mli b/infer/src/backend/RetainCyclesType.mli index cda6d68bf..5006e2c5b 100644 --- a/infer/src/backend/RetainCyclesType.mli +++ b/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 diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 3311daac0..737f51ed3 100644 --- a/infer/src/backend/dotty.ml +++ b/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. *) diff --git a/infer/src/backend/dotty.mli b/infer/src/backend/dotty.mli index 5525cd987..e4130b0e6 100644 --- a/infer/src/backend/dotty.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 813fedfc9..ea051fbf4 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 2984ccfdc..fbed1bd68 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/objc/errors/Makefile b/infer/tests/codetoanalyze/objc/errors/Makefile index 10ce17c2e..e8ae66d34 100644 --- a/infer/tests/codetoanalyze/objc/errors/Makefile +++ b/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 \ diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 3243d8194..e9d5a52be 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/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:] diff --git a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleLength3.m b/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleLength3.m new file mode 100644 index 000000000..444f076a2 --- /dev/null +++ b/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 + +@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; +}