diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml index bf6ffe270..5b1b8067d 100644 --- a/infer/src/IR/Procname.ml +++ b/infer/src/IR/Procname.ml @@ -257,6 +257,8 @@ module ObjC_Cpp = struct {class_name; method_name; kind; template_args; parameters} + let make_dealloc name = make name "dealloc" ObjCInstanceMethod Typ.NoTemplate [] + let get_class_name objc_cpp = Typ.Name.name objc_cpp.class_name let get_class_type_name objc_cpp = objc_cpp.class_name @@ -730,6 +732,8 @@ let make_java ~class_name ~return_type ~method_name ~parameters ~kind () = Java (Java.make ~class_name ~return_type ~method_name ~parameters ~kind ()) +let make_objc_dealloc name = ObjC_Cpp (ObjC_Cpp.make_dealloc name) + module Hashable = struct type nonrec t = t diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli index 242d5df75..7c76c8ded 100644 --- a/infer/src/IR/Procname.mli +++ b/infer/src/IR/Procname.mli @@ -262,6 +262,10 @@ val make_java : -> t (** Create a Java procedure name. *) +val make_objc_dealloc : Typ.Name.t -> t +(** Create a Objective-C dealloc name. This is a destructor for an Objective-C class. This procname + is given by the class name, since it is always an instance method with the name "dealloc" *) + val empty_block : t (** Empty block name. *) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 8a5f7e6e5..ba36f9687 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -142,12 +142,71 @@ module PulseTransferFunctions = struct exec_state_res + (* [get_dealloc_from_dynamic_types vars_types loc] returns a dealloc procname and vars and + type needed to execute a call to dealloc for the given variables for which the dynamic type + is an Objective-C class. *) + let get_dealloc_from_dynamic_types dynamic_types_unreachable = + let get_dealloc (var, name) = + let cls_typ = Typ.mk (Typ.Tstruct name) in + match Var.get_ident var with + | Some id when Typ.is_objc_class cls_typ -> + let ret_id = Ident.create_fresh Ident.knormal in + let dealloc = Procname.make_objc_dealloc name in + let typ = Typ.mk_ptr cls_typ in + Some (ret_id, id, typ, dealloc) + | _ -> + None + in + List.filter_map ~f:get_dealloc dynamic_types_unreachable + + + (* In the case of variables that point to Objective-C classes for which we have a dynamic type, we + add and execute calls to dealloc. The main advantage of adding this calls + is that some memory could be freed in dealloc, and we would be reporting a leak on it if we + didn't call it. *) + let execute_injected_dealloc_calls analysis_data vars astate location = + let used_ids = Stack.keys astate |> List.filter_map ~f:(fun var -> Var.get_ident var) in + Ident.update_name_generator used_ids ; + let call_dealloc (astate_list : Domain.t list) (ret_id, id, typ, dealloc) = + let ret = (ret_id, Typ.void) in + let call_flags = CallFlags.default in + let call_exp = Exp.Const (Cfun dealloc) in + let actuals = [(Exp.Var id, typ)] in + let call_instr = Sil.Call (ret, call_exp, actuals, location, call_flags) in + L.d_printfln ~color:Pp.Orange "@\nExecuting injected instr:%a@\n@." + (Sil.pp_instr Pp.text ~print_types:true) + call_instr ; + List.fold + ~f:(fun astates (astate : Domain.t) -> + let astate = + match astate with + | AbortProgram _ | ExitProgram _ -> + [astate] + | ContinueProgram astate -> + dispatch_call analysis_data ret call_exp actuals location call_flags astate + |> check_error_transform analysis_data ~f:Fn.id + in + List.rev_append astate astates ) + ~init:[] astate_list + in + let dynamic_types_unreachable = + PulseOperations.get_dynamic_type_unreachable_values vars astate + in + let dealloc_data = get_dealloc_from_dynamic_types dynamic_types_unreachable in + let ret_vars = List.map ~f:(fun (ret_id, _, _, _) -> Var.of_id ret_id) dealloc_data in + L.d_printfln ~color:Pp.Orange + "Executing injected call to dealloc for vars (%a) that are exiting the scope@." + (Pp.seq ~sep:"," Var.pp) vars ; + let astates = List.fold ~f:call_dealloc dealloc_data ~init:[Domain.ContinueProgram astate] in + (astates, ret_vars) + + let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data) _cfg_node (instr : Sil.instr) : Domain.t list = match astate with | AbortProgram _ -> (* We can also continue the analysis with the error state here - but there might be a risk we would get nonsense. *) + but there might be a risk we would get nonsense. *) [astate] | ExitProgram _ -> (* program already exited, simply propagate the exited state upwards *) @@ -192,8 +251,36 @@ module PulseTransferFunctions = struct dispatch_call analysis_data ret call_exp actuals loc call_flags astate |> check_error_transform analysis_data ~f:(fun id -> id) | Metadata (ExitScope (vars, location)) -> - let astate = PulseOperations.remove_vars vars location astate in - check_error_continue analysis_data astate + let remove_vars vars astates = + List.fold + ~f:(fun astates (astate : Domain.t) -> + match astate with + | AbortProgram _ | ExitProgram _ -> + [astate] + | ContinueProgram astate -> + let astate = + PulseOperations.remove_vars vars location astate + |> check_error_continue analysis_data + in + List.rev_append astate astates ) + ~init:[] astates + in + if Procname.is_java (Procdesc.get_proc_name proc_desc) then + remove_vars vars [Domain.ContinueProgram astate] + else + (* Here we add and execute calls to dealloc for Objective-C objects + before removing the variables *) + let astates, ret_vars = + execute_injected_dealloc_calls analysis_data vars astate location + in + (* OPTIM: avoid re-allocating [vars] when [ret_vars] is empty + (in particular if no ObjC objects are involved), but otherwise + assume [ret_vars] is potentially larger than [vars] and so + append [vars] to [ret_vars]. *) + let vars_to_remove = + if List.is_empty ret_vars then vars else List.rev_append vars ret_vars + in + remove_vars vars_to_remove astates | Metadata (VariableLifetimeBegins (pvar, _, location)) -> [PulseOperations.realloc_pvar pvar location astate |> Domain.continue] | Metadata (Abstract _ | Nullify _ | Skip) -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index a246cd2d2..984f42275 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -28,8 +28,10 @@ module type BaseDomainSig = sig val filter_addr : f:(AbstractValue.t -> bool) -> t -> t (** filter both heap and attrs *) - val filter_addr_with_discarded_attrs : f:(AbstractValue.t -> bool) -> t -> t * Attributes.t list - (** filter both heap and attrs with returning discarded attrs together *) + val filter_addr_with_discarded_addrs : + f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list + (** compute new state containing only reachable addresses in its heap and attributes, as well as + the list of discarded unreachable addresses *) val pp : F.formatter -> t -> unit end @@ -60,12 +62,12 @@ module BaseDomainCommon = struct update ~heap:heap' ~attrs:attrs' foot - let filter_addr_with_discarded_attrs ~f foot = + let filter_addr_with_discarded_addrs ~f foot = let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in - let attrs', discarded_attributes = - BaseAddressAttributes.filter_with_discarded_attrs (fun address _ -> f address) foot.attrs + let attrs', discarded_addresses = + BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs in - (update ~heap:heap' ~attrs:attrs' foot, discarded_attributes) + (update ~heap:heap' ~attrs:attrs' foot, discarded_addresses) end (** represents the post abstract state at each program point *) @@ -166,6 +168,9 @@ module Stack = struct let mem var astate = BaseStack.mem var (astate.post :> base_domain).stack let exists f astate = BaseStack.exists f (astate.post :> base_domain).stack + + let keys astate = + BaseStack.fold (fun key _ keys -> key :: keys) (astate.post :> base_domain).stack [] end module AddressAttributes = struct @@ -340,8 +345,8 @@ let discard_unreachable ({pre; post} as astate) = in let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in let live_addresses = AbstractValue.Set.union pre_addresses post_addresses in - let post_new, attrs_unreachable = - PostDomain.filter_addr_with_discarded_attrs + let post_new, discard_addresses = + PostDomain.filter_addr_with_discarded_addrs ~f:(fun address -> AbstractValue.Set.mem address live_addresses) post in @@ -350,7 +355,7 @@ let discard_unreachable ({pre; post} as astate) = if phys_equal pre_new pre && phys_equal post_new post then astate else {astate with pre= pre_new; post= post_new} in - (astate, live_addresses, attrs_unreachable) + (astate, live_addresses, discard_addresses) let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index f1b35d21e..06a74e820 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -32,8 +32,10 @@ module type BaseDomainSig = sig val filter_addr : f:(AbstractValue.t -> bool) -> t -> t (** filter both heap and attrs *) - val filter_addr_with_discarded_attrs : f:(AbstractValue.t -> bool) -> t -> t * Attributes.t list - (** filter both heap and attrs with returning discarded attrs together *) + val filter_addr_with_discarded_addrs : + f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list + (** compute new state containing only reachable addresses in its heap and attributes, as well as + the list of discarded unreachable addresses *) val pp : F.formatter -> t -> unit end @@ -82,6 +84,8 @@ module Stack : sig val mem : Var.t -> t -> bool val exists : (Var.t -> BaseStack.value -> bool) -> t -> bool + + val keys : t -> Var.t list end (** memory operations like {!BaseMemory} but that also take care of propagating facts to the @@ -142,9 +146,9 @@ val is_local : Var.t -> t -> bool val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option -val discard_unreachable : t -> t * AbstractValue.Set.t * Attributes.t list -(** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it - smaller, and retuns the new state, the live addresses, and the attributes of discarded addresses *) +val discard_unreachable : t -> t * AbstractValue.Set.t * AbstractValue.t list +(** garbage collect unreachable addresses in the state to make it smaller and return the new state, + the live addresses, and the discarded addresses that used to have attributes attached *) val add_skipped_call : Procname.t -> Trace.t -> t -> t diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 826d96ea4..7152cce9d 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -54,9 +54,9 @@ let empty = Graph.empty let filter = Graph.filter -let filter_with_discarded_attrs f x = +let filter_with_discarded_addrs f x = fold - (fun k v ((x, discarded) as acc) -> if f k v then acc else (Graph.remove k x, v :: discarded)) + (fun k v ((x, discarded) as acc) -> if f k v then acc else (Graph.remove k x, k :: discarded)) x (x, []) diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 2be1316de..1e9073911 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -14,8 +14,8 @@ val empty : t val filter : (AbstractValue.t -> Attributes.t -> bool) -> t -> t -val filter_with_discarded_attrs : - (AbstractValue.t -> Attributes.t -> bool) -> t -> t * Attributes.t list +val filter_with_discarded_addrs : + (AbstractValue.t -> Attributes.t -> bool) -> t -> t * AbstractValue.t list val find_opt : AbstractValue.t -> t -> Attributes.t option diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 39e6af37b..86ff89a8f 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -317,7 +317,7 @@ let mark_address_of_stack_variable history variable location address astate = AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate -let check_memory_leak_unreachable unreachable_attrs location astate = +let check_memory_leak_unreachable unreachable_addrs location astate = let check_memory_leak result attributes = let allocated_not_freed_opt = Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *)) @@ -337,12 +337,40 @@ let check_memory_leak_unreachable unreachable_attrs location astate = | _ -> result in - List.fold unreachable_attrs ~init:(Ok ()) ~f:check_memory_leak + List.fold unreachable_addrs ~init:(Ok ()) ~f:(fun res addr -> + match AbductiveDomain.AddressAttributes.find_opt addr astate with + | Some unreachable_attrs -> + check_memory_leak res unreachable_attrs + | None -> + res ) + + +let get_dynamic_type_unreachable_values vars astate = + (* For each unreachable address we find a root variable for it; if there is + more than one, it doesn't matter which *) + let find_var_opt astate addr = + Stack.fold + (fun var (var_addr, _) var_opt -> + if AbstractValue.equal addr var_addr then Some var else var_opt ) + astate None + in + let astate' = Stack.remove_vars vars astate in + let _, _, unreachable_addrs = AbductiveDomain.discard_unreachable astate' in + let res = + List.fold unreachable_addrs ~init:[] ~f:(fun res addr -> + (let open IOption.Let_syntax in + let* attrs = AbductiveDomain.AddressAttributes.find_opt addr astate in + let* typ = Attributes.get_dynamic_type attrs in + let+ var = find_var_opt astate addr in + (var, addr, typ) :: res) + |> Option.value ~default:res ) + in + List.map ~f:(fun (var, _, typ) -> (var, typ)) res -let remove_vars vars location astate = +let remove_vars vars location orig_astate = let astate = - List.fold vars ~init:astate ~f:(fun astate var -> + List.fold vars ~init:orig_astate ~f:(fun astate var -> match Stack.find_opt var astate with | Some (address, history) -> let astate = @@ -359,8 +387,8 @@ let remove_vars vars location astate = let astate' = Stack.remove_vars vars astate in if phys_equal astate' astate then Ok astate else - let astate, _, unreachable_attrs = AbductiveDomain.discard_unreachable astate' in - let+ () = check_memory_leak_unreachable unreachable_attrs location astate in + let astate, _, unreachable_addrs = AbductiveDomain.discard_unreachable astate' in + let+ () = check_memory_leak_unreachable unreachable_addrs location orig_astate in astate diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 7a5c11a67..ac73be6b8 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -114,6 +114,10 @@ val shallow_copy : -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** returns the address of a new cell with the same edges as the original *) +val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.Name.t) list +(** Given a list of variables, computes the unreachable values if the variables were removed from + the stack, then return the dynamic types of those values if they are available *) + val remove_vars : Var.t list -> Location.t -> t -> t access_result val check_address_escape : diff --git a/infer/tests/codetoanalyze/objc/pulse/DeallocCalls.m b/infer/tests/codetoanalyze/objc/pulse/DeallocCalls.m new file mode 100644 index 000000000..bc1e400b0 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/DeallocCalls.m @@ -0,0 +1,77 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include +#include + +@interface BufferContainer1 : NSObject + +@property char* buffer; + +@end + +@implementation BufferContainer1 + +- (instancetype)init { + _buffer = malloc(sizeof(char)); + return self; +} + +- (void)dealloc { + free(_buffer); +} + +@end + +@interface BufferContainer2 : NSObject + +@property char* buffer; + +@end + +@implementation BufferContainer2 + +- (instancetype)init { + _buffer = malloc(sizeof(char)); + return self; +} + +- (void)dealloc { +} + +@end + +@interface Araii : NSObject + +@property BufferContainer1* container; + +@end + +@implementation Araii + +- (instancetype)init { + _container = [[BufferContainer1 alloc] init]; + return self; +} + +@end + +/* b goes out of scope, this would cause b->_container to be leaked, +however, dealloc is called and _container is freed there, so no leak. */ +void memory_leak_raii_no_leak_ok() { + BufferContainer1* b = [[BufferContainer1 alloc] init]; +} + +/* b goes out of scope, this causes b->_container to be leaked. Even though +dealloc is called, _container is not freed there. */ +void memory_leak_raii_leak_bad() { + BufferContainer2* b = [[BufferContainer2 alloc] init]; +} + +/* a goes out of scope, this causes a->b->_container to be leaked. This is a FP +because dealloc is called, and it should call dealloc of b which would free +_container. This behaviour is still to be implemented. */ +void memory_leak_raii_no_leak_ok_FP() { Araii* a = [[Araii alloc] init]; } diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index c8900050a..2de2df09f 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,3 +1,5 @@ +codetoanalyze/objc/pulse/DeallocCalls.m, memory_leak_raii_leak_bad, 1, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `BufferContainer2.init` here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/DeallocCalls.m, memory_leak_raii_no_leak_ok_FP, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `Araii.init` here,when calling `BufferContainer1.init` here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MallocInObjC.m, leak_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc_no_fail` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.call_no_bridge_leak_bad, 1, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `MemoryLeaks.ret_no_bridge` here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks.cg_path_create_mutable_leak_bad:, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here]