From 32745b67aabf4966813ebc6b3ada841a14969c61 Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Thu, 7 Jan 2016 08:48:13 -0800 Subject: [PATCH] Add dotty information about retain cycle Summary: public Title - instead of just creating dot file in some location, include this information as part of bug description. Reviewed By: ddino Differential Revision: D2779941 fb-gh-sync-id: 6bfb02b --- infer/src/backend/abs.ml | 20 ++++++-------------- infer/src/backend/dotty.ml | 18 +++++++++++++----- infer/src/backend/dotty.mli | 3 +++ infer/src/backend/errdesc.ml | 4 ++-- infer/src/backend/errdesc.mli | 2 +- infer/src/backend/localise.ml | 4 ++-- infer/src/backend/localise.mli | 2 +- 7 files changed, 28 insertions(+), 25 deletions(-) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 16b950e93..5c431f5bb 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1132,20 +1132,12 @@ let should_raise_objc_leak prop hpred = Mleak_buckets.should_raise_objc_leak typ | _ -> None -let print_retain_cycle _prop cycle = +let get_retain_cycle_dotty _prop cycle = match _prop with - | None -> () + | None -> None | Some (Some _prop) -> - let loc = State.get_loc () in - let source_file = DB.source_file_to_string loc.Location.file in - let source_file'= Str.global_replace (Str.regexp_string "/") "_" source_file in - let dest_file_str = - (DB.filename_to_string (DB.Results_dir.specs_dir ())) ^ "/" ^ - source_file' ^ "_RETAIN_CYCLE_" ^ (Location.to_string loc) ^ ".dot" in - L.d_strln ("Printing dotty proposition for retain cycle in :"^dest_file_str); - Prop.d_prop _prop; L.d_strln ""; - Dotty.dotty_prop_to_dotty_file dest_file_str _prop cycle - | _ -> () + Dotty.dotty_prop_to_str _prop cycle + | _ -> None let get_var_retain_cycle _prop = let sigma = Prop.get_sigma _prop in @@ -1300,9 +1292,9 @@ let check_junk ?original_prop pname tenv prop = Mleak_buckets.should_raise_cpp_leak () | _ -> None in let exn_retain_cycle cycle = - print_retain_cycle original_prop cycle; + let cycle_dotty = get_retain_cycle_dotty original_prop cycle in let desc = Errdesc.explain_retain_cycle - (remove_opt original_prop) cycle (State.get_loc ()) in + (remove_opt original_prop) cycle (State.get_loc ()) cycle_dotty in Exceptions.Retain_cycle (remove_opt original_prop, hpred, desc, try assert false with Assert_failure x -> x) in diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index cc71245d2..b10af1578 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -926,16 +926,24 @@ let pp_dotty_prop_list_in_path f plist prev_n curr_n = with exn when exn_not_failure exn -> () +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_prop_to_str prop cycle = + try + Some (pp_to_string pp_dotty_prop (prop, cycle)) + with exn when exn_not_failure exn -> None + (* create a dotty file with a single proposition *) let dotty_prop_to_dotty_file fname prop cycle = try let out_dot = open_out fname in let fmt_dot = Format.formatter_of_out_channel out_dot in - reset_proposition_counter (); - Format.fprintf fmt_dot "@\n@\n@\ndigraph main { \nnode [shape=box]; @\n"; - Format.fprintf fmt_dot "@\n compound = true; rankdir =LR; @\n"; - pp_dotty fmt_dot Generic_proposition prop (Some cycle); - Format.fprintf fmt_dot "@\n}"; + pp_dotty_prop fmt_dot (prop, cycle); close_out out_dot with exn when exn_not_failure exn -> () diff --git a/infer/src/backend/dotty.mli b/infer/src/backend/dotty.mli index a9ec5020a..c6172c08e 100644 --- a/infer/src/backend/dotty.mli +++ b/infer/src/backend/dotty.mli @@ -47,6 +47,9 @@ val pp_speclist_dotty_file : DB.filename -> Prop.normal Specs.spec list -> unit val dotty_prop_to_dotty_file : string -> Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> unit +val dotty_prop_to_str : Prop.normal Prop.t -> + ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> string option + (** reset the counter used for node and heap identifiers *) val reset_node_counter : unit -> unit diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 0bf8b97ca..1e1ae26ee 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -963,8 +963,8 @@ let explain_return_expression_required loc typ = Localise.desc_return_expression_required typ_str loc (** Explain retain cycle value error *) -let explain_retain_cycle prop cycle loc = - Localise.desc_retain_cycle prop cycle loc +let explain_retain_cycle prop cycle loc dotty_str = + Localise.desc_retain_cycle prop cycle loc dotty_str (** Explain a tainted value error *) let explain_tainted_value_reaching_sensitive_function e taint_fun sensitive_fun loc = diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index e9b316329..d88d595d7 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -105,7 +105,7 @@ val explain_return_statement_missing : Location.t -> Localise.error_desc (** explain a retain cycle *) val explain_retain_cycle : Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> - Location.t -> Localise.error_desc + Location.t -> string option -> Localise.error_desc (** explain unary minus applied to unsigned expression *) val explain_unary_minus_applied_to_unsigned_expression : diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index bf126fcae..8ace3bf44 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -668,7 +668,7 @@ let desc_return_expression_required typ_str loc = (at_line tags loc) in { no_desc with descriptions = [description]; tags = !tags } -let desc_retain_cycle prop cycle loc = +let desc_retain_cycle prop cycle loc cycle_dotty = Logging.d_strln "Proposition with retain cycle:"; Prop.d_prop prop; Logging.d_strln ""; let ct = ref 1 in @@ -697,7 +697,7 @@ let desc_retain_cycle prop cycle loc = IList.iter do_edge cycle; let desc = Format.sprintf "Retain cycle involving the following objects: %s %s" !str_cycle (at_line tags loc) in - { no_desc with descriptions = [desc]; tags = !tags } + { no_desc with descriptions = [desc]; tags = !tags; dotty = cycle_dotty } let desc_return_statement_missing loc = let tags = Tags.create () in diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index 158decaf6..17adc3335 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -222,7 +222,7 @@ val desc_return_expression_required : string -> Location.t -> error_desc val desc_retain_cycle : Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> - Location.t -> error_desc + Location.t -> string option -> error_desc val desc_return_statement_missing : Location.t -> error_desc