diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 37b516abc..7fda7dbaa 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -207,14 +207,9 @@ let hpred_get_lhs h = (** {2 Comparision and Inspection Functions} *) -let has_objc_ref_counter tenv hpred = - match hpred with - | Hpointsto (_, _, Sizeof {typ= {desc= Tstruct name}}) -> ( - match Tenv.lookup tenv name with - | Some {fields} -> - List.exists ~f:Typ.Struct.is_objc_ref_counter_field fields - | _ -> - false ) +let is_objc_object = function + | Hpointsto (_, _, Sizeof {typ}) -> + Typ.is_objc_class typ | _ -> false @@ -1066,6 +1061,8 @@ let hpred_list_get_lexps (filter: Exp.t -> bool) (hlist: hpred list) : Exp.t lis List.filter ~f:filter lexps +let hpred_entries hpred = hpred_get_lexp [] hpred + (** {2 Functions for computing program variables} *) let rec exp_fpv e = match (e : Exp.t) with diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index 668a0ec87..afdd39a8d 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -255,7 +255,7 @@ val exp_compact : sharing_env -> Exp.t -> Exp.t val hpred_compact : sharing_env -> hpred -> hpred (** Return a compact representation of the exp *) -val has_objc_ref_counter : Tenv.t -> hpred -> bool +val is_objc_object : hpred -> bool (** {2 Comparision And Inspection Functions} *) val zero_value_of_numerical_type_option : Typ.t -> Exp.t option @@ -452,6 +452,8 @@ val atom_list_expmap : (Exp.t -> Exp.t) -> atom list -> atom list val hpred_list_get_lexps : (Exp.t -> bool) -> hpred list -> Exp.t list +val hpred_entries : hpred -> Exp.t list + (** {2 Function for computing lexps in sigma} *) val exp_fpv : Exp.t -> Pvar.t list diff --git a/infer/src/backend/RetainCycles.ml b/infer/src/backend/RetainCycles.ml new file mode 100644 index 000000000..b56b0e402 --- /dev/null +++ b/infer/src/backend/RetainCycles.ml @@ -0,0 +1,200 @@ +(* + * 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. + *) +module L = Logging +module F = Format + +let get_cycle root prop = + 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 "" + 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 + | [] -> + (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) + else + let visited' = fst et_src :: visited in + let res = + match get_points_to e 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' + | _ -> + (path, false) + (* check for lists *) + in + if snd res then res else dfs e_root et_src path el' visited' + 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 + (* 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 ) + else ( + L.d_strln "NO cycle found from root" ; + [] ) + | _ -> + L.d_strln "Root exp is not an allocated object. No cycle found" ; + [] + + +let get_retain_cycle_dotty prop_ cycle = + match prop_ with + | None -> + None + | Some Some prop_ -> + Dotty.dotty_prop_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 + 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 + 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' + in + do_sigma sigma + + +(** 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 = + (* returns items annotation for field fn in struct t *) + let get_item_annotation (t: Typ.t) fn = + match t.desc with + | Tstruct name + -> ( + let equal_fn (fn', _, _) = Typ.Fieldname.equal fn fn' in + match Tenv.lookup tenv name with + | Some {fields; statics} -> + List.find ~f:equal_fn (fields @ statics) |> Option.value_map ~f:trd3 ~default:[] + | None -> + [] ) + | _ -> + [] + in + let rec has_weak_or_unretained_or_assign params = + match params with + | [] -> + false + | att :: _ + when String.equal Config.unsafe_unret att || String.equal Config.weak att + || String.equal Config.assign att -> + true + | _ :: params' -> + has_weak_or_unretained_or_assign params' + in + let do_annotation ((a: Annot.t), _) = + ( String.equal a.class_name Config.property_attributes + || String.equal a.class_name Config.ivar_attributes ) + && has_weak_or_unretained_or_assign a.parameters + in + let rec do_cycle c = + match c with + | [] -> + false + | ((_, t), fn, _) :: c' -> + let ia = get_item_annotation t fn in + if List.exists ~f:do_annotation ia then true else do_cycle c' + in + do_cycle cycle + + +let exn_retain_cycle original_prop hpred cycle = + let cycle_dotty = get_retain_cycle_dotty original_prop cycle in + let desc = Errdesc.explain_retain_cycle cycle (State.get_loc ()) cycle_dotty in + Exceptions.Retain_cycle (hpred, desc, __POS__) + + +let report_cycle tenv hpred original_prop = + (* When there is a cycle in objc we ignore it + 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) + diff --git a/infer/src/backend/RetainCycles.mli b/infer/src/backend/RetainCycles.mli new file mode 100644 index 000000000..f6e3f0697 --- /dev/null +++ b/infer/src/backend/RetainCycles.mli @@ -0,0 +1,10 @@ +(* + * 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. + *) + +val report_cycle : Tenv.t -> Sil.hpred -> Prop.normal Prop.t option option -> bool * exn diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index f5aac8e5d..40d32952d 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -949,16 +949,6 @@ module HpredSet = Caml.Set.Make (struct let compare = Sil.compare_hpred ~inst:false end) -let hpred_entries hpred = - match hpred with - | Sil.Hpointsto (e, _, _) -> - [e] - | Sil.Hlseg (_, _, e, _, _) -> - [e] - | Sil.Hdllseg (_, _, e1, _, _, e2, _) -> - [e1; e2] - - (** find the id's in sigma reachable from the given roots *) let sigma_reachable root_fav sigma = let fav_to_set fav = Ident.idlist_to_idset (Sil.fav_to_list fav) in @@ -967,7 +957,7 @@ let sigma_reachable root_fav sigma = let do_hpred hpred = let hp_fav_set = fav_to_set (Sil.hpred_fav hpred) in let add_entry e = edges := (e, hp_fav_set) :: !edges in - List.iter ~f:add_entry (hpred_entries hpred) + List.iter ~f:add_entry (Sil.hpred_entries hpred) in List.iter ~f:do_hpred sigma ; let edge_fires (e, _) = @@ -999,76 +989,9 @@ let sigma_reachable root_fav sigma = !reach_set -let get_cycle root prop = - 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 "" - 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 - | [] -> - (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) - else - let visited' = fst et_src :: visited in - let res = - match get_points_to e 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' - | _ -> - (path, false) - (* check for lists *) - in - if snd res then res else dfs e_root et_src path el' visited' - 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 - (* 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 ) - else ( - L.d_strln "NO cycle found from root" ; - [] ) - | _ -> - L.d_strln "Root exp is not an allocated object. No cycle found" ; - [] - - (** Check whether the hidden counter field of a struct representing an objective-c object is - positive, and whether the leak is part of the specified buckets. In the positive case, it - returns the bucket *) + positive, and whether the leak is part of the specified buckets. In the positive case, it + returns the bucket *) let should_raise_objc_leak hpred = match hpred with | Sil.Hpointsto @@ -1079,113 +1002,6 @@ let should_raise_objc_leak hpred = None -let get_retain_cycle_dotty prop_ cycle = - match prop_ with - | None -> - None - | Some Some prop_ -> - Dotty.dotty_prop_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 - 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 - 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' - in - do_sigma sigma - - -let remove_opt prop_ = match prop_ with Some Some p -> p | _ -> Prop.prop_emp - -(** 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 = - (* returns items annotation for field fn in struct t *) - let get_item_annotation (t: Typ.t) fn = - match t.desc with - | Tstruct name - -> ( - let equal_fn (fn', _, _) = Typ.Fieldname.equal fn fn' in - match Tenv.lookup tenv name with - | Some {fields; statics} -> - List.find ~f:equal_fn (fields @ statics) |> Option.value_map ~f:trd3 ~default:[] - | None -> - [] ) - | _ -> - [] - in - let rec has_weak_or_unretained_or_assign params = - match params with - | [] -> - false - | att :: _ - when String.equal Config.unsafe_unret att || String.equal Config.weak att - || String.equal Config.assign att -> - true - | _ :: params' -> - has_weak_or_unretained_or_assign params' - in - let do_annotation ((a: Annot.t), _) = - ( String.equal a.class_name Config.property_attributes - || String.equal a.class_name Config.ivar_attributes ) - && has_weak_or_unretained_or_assign a.parameters - in - let rec do_cycle c = - match c with - | [] -> - false - | ((_, t), fn, _) :: c' -> - let ia = get_item_annotation t fn in - if List.exists ~f:do_annotation ia then true else do_cycle c' - in - do_cycle cycle - - let check_observer_is_unsubscribed_deallocation tenv prop e = let pvar_opt = match Attribute.get_resource tenv prop e with @@ -1240,7 +1056,7 @@ let check_junk ?original_prop pname tenv prop = let set3 = sigma_reachable fav2 sigma in Ident.IdentSet.mem id set3 in - let entries = hpred_entries hpred 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 @@ -1258,7 +1074,7 @@ let check_junk ?original_prop pname tenv prop = | [] -> List.rev sigma_done | hpred :: sigma_todo' -> - let entries = hpred_entries hpred in + let entries = Sil.hpred_entries hpred in if should_remove_hpred entries then let part = if fp_part then "footprint" else "normal" in L.d_strln (".... Prop with garbage in " ^ part ^ " part ....") ; @@ -1317,11 +1133,6 @@ let check_junk ?original_prop pname tenv prop = | _ -> None in - let exn_retain_cycle cycle = - let cycle_dotty = get_retain_cycle_dotty original_prop cycle in - let desc = Errdesc.explain_retain_cycle cycle (State.get_loc ()) cycle_dotty in - Exceptions.Retain_cycle (hpred, desc, __POS__) - in let exn_leak = Exceptions.Leak ( fp_part @@ -1336,15 +1147,7 @@ let check_junk ?original_prop pname tenv prop = | Some PredSymb.Awont_leak, Rmemory _ -> (true, exn_leak) | Some _, Rmemory Mobjc when hpred_in_cycle hpred -> - (* When there is a cycle in objc we ignore it - only if it's empty or it has weak or unsafe_unretained fields. - Otherwise we report a retain cycle. *) - 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 cycle) + RetainCycles.report_cycle tenv hpred original_prop | Some _, Rmemory Mobjc | Some _, Rmemory Mnew | Some _, Rmemory Mnew_array @@ -1360,12 +1163,11 @@ let check_junk ?original_prop pname tenv prop = (false, exn_leak) | Some _, Rlock -> (false, exn_leak) - | _ when hpred_in_cycle hpred && Sil.has_objc_ref_counter tenv hpred -> - (* When it's a cycle and the object has a ref counter then + | _ when hpred_in_cycle hpred && Sil.is_objc_object hpred -> + (* 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 *) - let cycle = get_var_retain_cycle (remove_opt original_prop) in - (Int.equal (List.length cycle) 0, exn_retain_cycle cycle) + RetainCycles.report_cycle tenv hpred original_prop | _ -> (Config.curr_language_is Config.Java, exn_leak) in diff --git a/infer/tests/codetoanalyze/objc/errors/Makefile b/infer/tests/codetoanalyze/objc/errors/Makefile index 3395e781b..1c94de377 100644 --- a/infer/tests/codetoanalyze/objc/errors/Makefile +++ b/infer/tests/codetoanalyze/objc/errors/Makefile @@ -87,6 +87,7 @@ SOURCES_BUCKET_ALL = \ SOURCES_ARC = \ field_superclass/SubtypingExample.m \ initialization/struct_initlistexpr.c \ + memory_leaks_benchmark/RetainCycleExampleWeak.m \ memory_leaks_benchmark/RetainReleaseExampleBucketingArc.m \ memory_leaks_benchmark/retain_cycle.m \ memory_leaks_benchmark/retain_cycle2.m \ diff --git a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleExampleWeak.m b/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleExampleWeak.m new file mode 100644 index 000000000..7a64bd730 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleExampleWeak.m @@ -0,0 +1,50 @@ +/* + * 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. + */ +#import + +@class AFeed; + +@interface Adapter : NSObject + +@property(nonatomic, strong) AFeed* feed; + +@end + +@implementation Adapter + +@end + +@interface AFeed : NSObject + +@property(nonatomic, weak) Adapter* adapter; + +@end + +@implementation AFeed + +@end + +@interface RetainCycleExampleWeak : NSObject + +@property(nonatomic, strong) AFeed* feed; + +@end + +@implementation RetainCycleExampleWeak + +- (void)test { + _feed.adapter.feed = _feed; +} + +- (void)main1 { + RetainCycleExampleWeak* b = [RetainCycleExampleWeak new]; + [b test]; +} + +@end