From d7dc9b38f78417cfa57e5da01d2e87885ce65a7a Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Tue, 12 Dec 2017 11:09:50 -0800 Subject: [PATCH] [retain cycles] Refactoring of computing cycles using dedicated data structure Reviewed By: mbouaziz Differential Revision: D6534576 fbshipit-source-id: 119b618 --- infer/src/IR/Localise.ml | 57 +++++------- infer/src/IR/Localise.mli | 4 +- infer/src/backend/RetainCycles.ml | 124 +++++++++---------------- infer/src/backend/RetainCycles.mli | 2 +- infer/src/backend/RetainCyclesType.ml | 42 +++++++++ infer/src/backend/RetainCyclesType.mli | 25 +++++ infer/src/backend/abs.ml | 16 +++- infer/src/backend/dotty.ml | 21 ++++- infer/src/backend/dotty.mli | 3 +- infer/src/backend/errdesc.mli | 4 +- 10 files changed, 170 insertions(+), 128 deletions(-) create mode 100644 infer/src/backend/RetainCyclesType.ml create mode 100644 infer/src/backend/RetainCyclesType.mli diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 2cf0b2f60..99a33e8d5 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -891,41 +891,34 @@ let desc_return_expression_required typ_str loc = let desc_retain_cycle cycle loc cycle_dotty = Logging.d_strln "Proposition with retain cycle:" ; - let ct = ref 1 in let tags = Tags.create () in - let str_cycle = ref "" in - let remove_old s = - match Str.split_delim (Str.regexp_string "&old_") s with [_; s'] -> s' | _ -> s - in - let do_edge ((se, _), f, _) = - match se with - | Sil.Eexp (Exp.Lvar pvar, _) when Pvar.equal pvar Sil.block_pvar -> - str_cycle - := !str_cycle ^ " (" ^ string_of_int !ct ^ ") a block capturing " - ^ MF.monospaced_to_string (Typ.Fieldname.to_string f) ^ "; " ; - ct := !ct + 1 - | Sil.Eexp ((Exp.Lvar pvar as e), _) -> - let e_str = Exp.to_string e in - let e_str = if Pvar.is_seed pvar then remove_old e_str else e_str in - str_cycle - := !str_cycle ^ " (" ^ string_of_int !ct ^ ") object " ^ e_str ^ " retaining " - ^ MF.monospaced_to_string (e_str ^ "." ^ Typ.Fieldname.to_string f) ^ ", " ; - ct := !ct + 1 - | Sil.Eexp (Exp.Sizeof {typ}, _) -> - let step = - " (" ^ string_of_int !ct ^ ") an object of " - ^ MF.monospaced_to_string (Typ.to_string typ) - ^ " retaining another object via instance variable " - ^ MF.monospaced_to_string (Typ.Fieldname.to_string f) ^ ", " - in - str_cycle := !str_cycle ^ step ; - ct := !ct + 1 - | _ -> - () + let desc_retain_cycle (cycle: RetainCyclesType.t) = + let open RetainCyclesType in + let remove_old s = + match Str.split_delim (Str.regexp_string "&old_") s with [_; s'] -> s' | _ -> s + in + let do_edge index_ edge = + let index = index_ + 1 in + let from_exp_str = + match edge.rc_from.rc_node_exp with + | Exp.Lvar pvar when Pvar.equal pvar Sil.block_pvar -> + "a block capturing" + | Exp.Lvar pvar as e -> + let e_str = Exp.to_string e in + if Pvar.is_seed pvar then remove_old e_str else e_str + | _ -> + Format.sprintf "An object of type %s" + (MF.monospaced_to_string (Typ.to_string edge.rc_from.rc_node_typ)) + in + Format.sprintf "(%d) %s retaining another object via instance variable %s, " index + from_exp_str + (MF.monospaced_to_string (Typ.Fieldname.to_string edge.rc_field.rc_field_name)) + in + let cycle_str = List.mapi ~f:do_edge cycle.rc_elements in + String.concat cycle_str ~sep:" " in - List.iter ~f:do_edge cycle ; let desc = - Format.sprintf "Retain cycle involving the following objects: %s %s" !str_cycle + Format.sprintf "Retain cycle involving the following objects:%s %s" (desc_retain_cycle cycle) (at_line tags loc) in {no_desc with descriptions= [desc]; tags= !tags; dotty= cycle_dotty} diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index baad8b7fc..9b5a6714b 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -201,9 +201,7 @@ val desc_precondition_not_met : pnm_kind option -> Typ.Procname.t -> Location.t val desc_return_expression_required : string -> Location.t -> error_desc -val desc_retain_cycle : - ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> Location.t -> string option - -> error_desc +val desc_retain_cycle : RetainCyclesType.t -> Location.t -> string option -> error_desc val registered_observer_being_deallocated_str : string -> string diff --git a/infer/src/backend/RetainCycles.ml b/infer/src/backend/RetainCycles.ml index b56b0e402..a862970ce 100644 --- a/infer/src/backend/RetainCycles.ml +++ b/infer/src/backend/RetainCycles.ml @@ -10,64 +10,54 @@ module L = Logging module F = Format let get_cycle root prop = + let open RetainCyclesType in let sigma = prop.Prop.sigma in let get_points_to e = - match e with - | Sil.Eexp (e', _) -> - List.find - ~f:(fun hpred -> - match hpred with Sil.Hpointsto (e'', _, _) -> Exp.equal e'' e' | _ -> false) - sigma - | _ -> - None - in - let print_cycle cyc = - L.d_str "Cycle= " ; - List.iter - ~f:(fun ((e, t), f, e') -> - match (e, e') with - | Sil.Eexp (e, _), Sil.Eexp (e', _) -> - L.d_str - ( "(" ^ Exp.to_string e ^ ": " ^ Typ.to_string t ^ ", " ^ Typ.Fieldname.to_string f - ^ ", " ^ Exp.to_string e' ^ ")" ) - | _ -> - ()) - cyc ; - L.d_strln "" + List.find + ~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. - Returns a pair (path, bool) where path is a list of edges ((e1,type_e1),f,e2) - describing the path to e_root and bool is true if e_root is reached. *) - let rec dfs e_root et_src path el visited = - match el with + 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 = + match fields with | [] -> (path, false) - | (f, e) :: el' -> - if Sil.equal_strexp e e_root then ((et_src, f, e) :: path, true) - else if List.mem ~equal:Sil.equal_strexp visited e then (path, false) + | (field, Sil.Eexp (f_exp, f_inst)) :: el' -> + if Exp.equal f_exp root_node.rc_node_exp then + let rc_field = {rc_field_name= field; rc_field_inst= f_inst} in + let edge = {rc_from= from_node; rc_field} in + (edge :: path, true) + else if List.mem ~equal:Exp.equal visited f_exp then (path, false) else - let visited' = fst et_src :: visited in + let visited' = from_node.rc_node_exp :: visited in let res = - match get_points_to e with + match get_points_to f_exp with | None -> (path, false) - | Some Sil.Hpointsto (_, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) -> - dfs e_root (e, te) ((et_src, f, e) :: path) fl visited' + | Some Sil.Hpointsto (_, Sil.Estruct (new_fields, _), Exp.Sizeof {typ= te}) -> + let rc_field = {rc_field_name= field; rc_field_inst= f_inst} in + let edge = {rc_from= from_node; rc_field} in + let rc_to = {rc_node_exp= f_exp; rc_node_typ= te} in + dfs root_node rc_to (edge :: path) new_fields visited' | _ -> (path, false) (* check for lists *) in - if snd res then res else dfs e_root et_src path el' visited' + if snd res then res else dfs root_node from_node path el' visited' + | _ -> + (path, false) in L.d_strln "Looking for cycle with root expression: " ; Sil.d_hpred root ; L.d_strln "" ; match root with | Sil.Hpointsto (e_root, Sil.Estruct (fl, _), Exp.Sizeof {typ= te}) -> - let se_root = Sil.Eexp (e_root, Sil.Inone) in + 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 se_root (se_root, te) [] fl [] in - if res then ( print_cycle pot_cycle ; pot_cycle ) + let pot_cycle, res = dfs se_root se_root [] fl [] in + if res then pot_cycle else ( L.d_strln "NO cycle found from root" ; [] ) @@ -81,45 +71,13 @@ let get_retain_cycle_dotty prop_ cycle = | None -> None | Some Some prop_ -> - Dotty.dotty_prop_to_str prop_ cycle + Dotty.dotty_retain_cycle_to_str prop_ cycle | _ -> None let get_var_retain_cycle prop_ = let sigma = prop_.Prop.sigma in - let is_pvar v h = - match h with - | Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.equal_strexp v v' -> - true - | _ -> - false - in - let is_hpred_block v h = - match (h, v) with - | Sil.Hpointsto (e, _, Exp.Sizeof {typ}), Sil.Eexp (e', _) - when Exp.equal e e' && Typ.is_block_type typ -> - true - | _, _ -> - false - in - let find v = List.find ~f:(is_pvar v) sigma |> Option.map ~f:Sil.hpred_get_lhs in - let find_block v = - if List.exists ~f:(is_hpred_block v) sigma then Some (Exp.Lvar Sil.block_pvar) else None - in - let sexp e = Sil.Eexp (e, Sil.Inone) in - let find_or_block ((e, t), f, e') = - match find e with - | Some pvar -> - [((sexp pvar, t), f, e')] - | _ -> - match find_block e with - | Some blk -> - [((sexp blk, t), f, e')] - | _ -> - let sizeof = {Exp.typ= t; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in - [((sexp (Exp.Sizeof sizeof), t), f, e')] - in (* 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 @@ -130,16 +88,16 @@ let get_var_retain_cycle prop_ = [] | hp :: sigma' -> let cycle = get_cycle hp prop_ in - L.d_strln "Filtering pvar in cycle " ; - let cycle' = List.concat_map ~f:find_or_block cycle in - if List.is_empty cycle' then do_sigma sigma' else cycle' + if List.is_empty cycle then do_sigma sigma' else cycle in - do_sigma sigma + let cycle_elements = do_sigma sigma in + RetainCyclesType.create_cycle cycle_elements (** Checks if cycle has fields (derived from a property or directly defined as ivar) with attributes weak/unsafe_unretained/assing *) let cycle_has_weak_or_unretained_or_assign_field tenv cycle = + let open RetainCyclesType in (* returns items annotation for field fn in struct t *) let get_item_annotation (t: Typ.t) fn = match t.desc with @@ -171,14 +129,15 @@ let cycle_has_weak_or_unretained_or_assign_field tenv cycle = && has_weak_or_unretained_or_assign a.parameters in let rec do_cycle c = + let open RetainCyclesType in match c with | [] -> false - | ((_, t), fn, _) :: c' -> - let ia = get_item_annotation t fn in + | edge :: c' -> + let ia = get_item_annotation edge.rc_from.rc_node_typ edge.rc_field.rc_field_name in if List.exists ~f:do_annotation ia then true else do_cycle c' in - do_cycle cycle + do_cycle cycle.rc_elements let exn_retain_cycle original_prop hpred cycle = @@ -192,9 +151,10 @@ let report_cycle tenv hpred original_prop = 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 cycle = get_var_retain_cycle (remove_opt original_prop) in - let ignore_cycle = - Int.equal (List.length cycle) 0 || cycle_has_weak_or_unretained_or_assign_field tenv cycle - in - (ignore_cycle, exn_retain_cycle original_prop hpred cycle) + match get_var_retain_cycle (remove_opt original_prop) with + | Some cycle when not (cycle_has_weak_or_unretained_or_assign_field tenv cycle) -> + RetainCyclesType.print_cycle cycle ; + Some (exn_retain_cycle original_prop hpred cycle) + | _ -> + None diff --git a/infer/src/backend/RetainCycles.mli b/infer/src/backend/RetainCycles.mli index f6e3f0697..172069858 100644 --- a/infer/src/backend/RetainCycles.mli +++ b/infer/src/backend/RetainCycles.mli @@ -7,4 +7,4 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -val report_cycle : Tenv.t -> Sil.hpred -> Prop.normal Prop.t option option -> bool * exn +val report_cycle : Tenv.t -> Sil.hpred -> Prop.normal Prop.t option option -> exn option diff --git a/infer/src/backend/RetainCyclesType.ml b/infer/src/backend/RetainCyclesType.ml new file mode 100644 index 000000000..a505cfbcb --- /dev/null +++ b/infer/src/backend/RetainCyclesType.ml @@ -0,0 +1,42 @@ +(* + * Copyright (c) 2017 - 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. + *) +type retain_cycle_node = {rc_node_exp: Exp.t; rc_node_typ: Typ.t} + +type retain_cycle_field_objc = {rc_field_name: Typ.Fieldname.t; rc_field_inst: Sil.inst} + +type retain_cycle_edge = {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc} + +type t = {rc_elements: retain_cycle_edge list; rc_head: retain_cycle_edge} + +let create_cycle cycle = + match cycle with hd :: _ -> Some {rc_elements= cycle; rc_head= hd} | [] -> None + + +let retain_cycle_node_to_string (node: retain_cycle_node) = + Format.sprintf "%s : %s" (Exp.to_string node.rc_node_exp) (Typ.to_string node.rc_node_typ) + + +let retain_cycle_field_to_string (field: retain_cycle_field_objc) = + Format.sprintf "%s[%s]" + (Typ.Fieldname.to_string field.rc_field_name) + (Sil.inst_to_string field.rc_field_inst) + + +let retain_cycle_edge_to_string (edge: retain_cycle_edge) = + Format.sprintf "%s ->{%s}" + (retain_cycle_node_to_string edge.rc_from) + (retain_cycle_field_to_string edge.rc_field) + + +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) diff --git a/infer/src/backend/RetainCyclesType.mli b/infer/src/backend/RetainCyclesType.mli new file mode 100644 index 000000000..09a6a7320 --- /dev/null +++ b/infer/src/backend/RetainCyclesType.mli @@ -0,0 +1,25 @@ +(* + * Copyright (c) 2017 - 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. + *) + +type retain_cycle_node = {rc_node_exp: Exp.t; rc_node_typ: Typ.t} + +type retain_cycle_field_objc = {rc_field_name: Typ.Fieldname.t; rc_field_inst: Sil.inst} + +type retain_cycle_edge = {rc_from: retain_cycle_node; rc_field: retain_cycle_field_objc} + +(** 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} + +val retain_cycle_to_string : t -> string + +val print_cycle : t -> unit + +val create_cycle : retain_cycle_edge list -> t option +(** Creates a cycle if the list is non-empty *) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index f85122e3c..b890c8b25 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1131,8 +1131,12 @@ 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 -> - RetainCycles.report_cycle tenv hpred original_prop + | Some _, Rmemory Mobjc when hpred_in_cycle hpred -> ( + 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 @@ -1148,11 +1152,17 @@ 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 hpred_in_cycle hpred && 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 + with + | Some exn -> + (false, exn) + | None -> + (true, exn_leak) ) | _ -> (Config.curr_language_is Config.Java, exn_leak) in diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 5da6d6710..8fed5fd0f 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -1097,8 +1097,24 @@ let pp_dotty_prop fmt (prop, cycle) = Format.fprintf fmt "@\n}" -let dotty_prop_to_str prop cycle = - try Some (F.asprintf "%a" pp_dotty_prop (prop, cycle)) +let dotty_retain_cycle_to_str prop (cycle: RetainCyclesType.t) = + let open RetainCyclesType in + let rec cycle_to_list elements = + match elements with + | edge1 :: edge2 :: rest -> + ( edge1.rc_from.rc_node_exp + , edge1.rc_field.rc_field_name + , Sil.Eexp (edge2.rc_from.rc_node_exp, Sil.Inone) ) + :: cycle_to_list (edge2 :: rest) + | [edge] -> + [ ( edge.rc_from.rc_node_exp + , edge.rc_field.rc_field_name + , Sil.Eexp (cycle.rc_head.rc_from.rc_node_exp, 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 @@ -1717,3 +1733,4 @@ let print_specs_xml signature specs loc fmt = [xml_signature; xml_specifications] in Io_infer.Xml.pp_document true fmt proc_summary + diff --git a/infer/src/backend/dotty.mli b/infer/src/backend/dotty.mli index aea4023af..9a9034e2d 100644 --- a/infer/src/backend/dotty.mli +++ b/infer/src/backend/dotty.mli @@ -49,8 +49,7 @@ val dotty_prop_to_dotty_file : string -> Prop.normal Prop.t -> ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> unit -val dotty_prop_to_str : - Prop.normal Prop.t -> ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> string option +val dotty_retain_cycle_to_str : Prop.normal Prop.t -> RetainCyclesType.t -> string option val reset_node_counter : unit -> unit (** reset the counter used for node and heap identifiers *) diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 59cbf115e..28abafa1d 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -101,9 +101,7 @@ val explain_frontend_warning : string -> string option -> Location.t -> Localise val explain_return_statement_missing : Location.t -> Localise.error_desc (** explain a return statement missing *) -val explain_retain_cycle : - ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> Location.t -> string option - -> Localise.error_desc +val explain_retain_cycle : RetainCyclesType.t -> Location.t -> string option -> Localise.error_desc (** explain a retain cycle *) val explain_unary_minus_applied_to_unsigned_expression :