From 6f2b52fcc7d09f676bb9ce7c309ebc22ab8f8ada Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Mon, 6 Apr 2020 01:42:01 -0700 Subject: [PATCH] [pulse] Model Core Graphics create and copy functions Summary: This models all the Create and Copy functions from CoreGraphics, examples in the tests. These functions all allocate memory that needs to be manually released. The modelling of the release functions will happen in a following diff. Until then, we have some false positives in the tests. This check is currently in biabduction, and we aim to move it to Pulse. Reviewed By: jvillard Differential Revision: D20626395 fbshipit-source-id: b39eae2d9 --- infer/src/absint/PatternMatch.ml | 8 +++ infer/src/absint/PatternMatch.mli | 4 ++ infer/src/pulse/PulseAbductiveDomain.ml | 9 ++-- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseAttribute.ml | 9 ++-- infer/src/pulse/PulseAttribute.mli | 3 +- infer/src/pulse/PulseBaseAddressAttributes.ml | 4 +- .../src/pulse/PulseBaseAddressAttributes.mli | 2 +- infer/src/pulse/PulseDiagnostic.ml | 6 +-- infer/src/pulse/PulseDiagnostic.mli | 2 +- infer/src/pulse/PulseModels.ml | 18 +++++-- infer/src/pulse/PulseOperations.ml | 12 +++-- infer/src/pulse/PulseOperations.mli | 2 +- .../codetoanalyze/objc/pulse/MemoryLeaks.m | 49 +++++++++++++++++++ .../tests/codetoanalyze/objc/pulse/issues.exp | 5 ++ 15 files changed, 110 insertions(+), 25 deletions(-) create mode 100644 infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 84e76dac8..4c4c93c24 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -472,3 +472,11 @@ let is_override_of_java_lang_object_equals curr_pname = in String.equal (Procname.get_method curr_pname) "equals" && is_only_param_of_object_type (Procname.get_parameters curr_pname) + + +module ObjectiveC = struct + let is_core_graphics_create_or_copy _ procname = + String.is_prefix ~prefix:"CG" procname + && ( String.is_substring ~substring:"Create" procname + || String.is_substring ~substring:"Copy" procname ) +end diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli index 024aaeb00..faa4e8cf3 100644 --- a/infer/src/absint/PatternMatch.mli +++ b/infer/src/absint/PatternMatch.mli @@ -160,3 +160,7 @@ val has_same_signature : Procname.t -> (Procname.t -> bool) Staged.t val is_override_of_java_lang_object_equals : Procname.t -> bool (** Whether the method is an override of `java.lang.Object.equals(Object)` or `java.lang.Object.equals(Object)` itself *) + +module ObjectiveC : sig + val is_core_graphics_create_or_copy : Tenv.t -> string -> bool +end diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 96ad0602e..22d922b38 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -213,8 +213,8 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.invalidate address invalidation location) - let allocate address location astate = - map_post_attrs astate ~f:(BaseAddressAttributes.allocate address location) + let allocate procname address location astate = + map_post_attrs astate ~f:(BaseAddressAttributes.allocate procname address location) let add_one address attributes astate = @@ -696,8 +696,9 @@ module PrePost = struct (invalidation, add_call_to_trace proc_name call_location caller_history trace) | CItv (arith, trace) -> Attribute.CItv (arith, add_call_to_trace proc_name call_location caller_history trace) - | Allocated trace -> - Attribute.Allocated (add_call_to_trace proc_name call_location caller_history trace) + | Allocated (procname, trace) -> + Attribute.Allocated + (procname, add_call_to_trace proc_name call_location caller_history trace) | AddressOfCppTemporary _ | AddressOfStackVariable _ | BoItv _ diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 9300b7f88..decb2c4ca 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -77,7 +77,7 @@ module AddressAttributes : sig val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t + val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index a77ff4fba..6a67f3f12 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -28,7 +28,7 @@ module Attribute = struct type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t - | Allocated of Trace.t + | Allocated of Procname.t * Trace.t | CItv of CItv.t * Trace.t | BoItv of Itv.ItvPure.t | Closure of Procname.t @@ -76,8 +76,11 @@ module Attribute = struct F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history | AddressOfStackVariable (var, location, history) -> F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location - | Allocated trace -> - F.fprintf f "Allocated %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "allocation")) trace + | Allocated (procname, trace) -> + F.fprintf f "Allocated %a" + (Trace.pp + ~pp_immediate:(pp_string_if_debug ("allocation with " ^ Procname.to_string procname))) + trace | BoItv bo_itv -> F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv | Closure pname -> diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index ab061475b..d997e0ade 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -14,7 +14,8 @@ module ValueHistory = PulseValueHistory type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t - | Allocated of Trace.t + | Allocated of Procname.t * Trace.t + (** the {!Procname.t} is the function causing the allocation, eg [malloc] *) | CItv of CItv.t * Trace.t | BoItv of Itv.ItvPure.t | Closure of Procname.t diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 41f47c923..414e0b944 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -53,8 +53,8 @@ let invalidate (address, history) invalidation location memory = add_one address (Attribute.Invalid (invalidation, Immediate {location; history})) memory -let allocate (address, history) location memory = - add_one address (Attribute.Allocated (Immediate {location; history})) memory +let allocate procname (address, history) location memory = + add_one address (Attribute.Allocated (procname, Immediate {location; history})) memory let check_valid address attrs = diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index c2e8207c9..1bddc14ed 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -22,7 +22,7 @@ val add_one : AbstractValue.t -> Attribute.t -> t -> t val add : AbstractValue.t -> Attributes.t -> t -> t -val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t +val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 16fad52a7..70f227668 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -15,7 +15,7 @@ module ValueHistory = PulseValueHistory type t = | AccessToInvalidAddress of {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t} - | MemoryLeak of {allocation_trace: Trace.t; location: Location.t} + | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} let get_location = function @@ -67,7 +67,7 @@ let get_message = function F.asprintf "%a%a" pp_access_trace access_trace (pp_invalidation_trace invalidation_line invalidation) invalidation_trace - | MemoryLeak {location; allocation_trace} -> + | MemoryLeak {procname; location; allocation_trace} -> let allocation_line = let {Location.line; _} = Trace.get_outer_location allocation_trace in line @@ -75,7 +75,7 @@ let get_message = function let pp_allocation_trace fmt (trace : Trace.t) = match trace with | Immediate _ -> - F.fprintf fmt "by call to `malloc()`" + F.fprintf fmt "by call to `%a`" Procname.pp procname | ViaCall {f; _} -> F.fprintf fmt "by call to %a" CallEvent.describe f in diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index f07ffb7a5..ef5952e7d 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -14,7 +14,7 @@ module ValueHistory = PulseValueHistory type t = | AccessToInvalidAddress of {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t} - | MemoryLeak of {allocation_trace: Trace.t; location: Location.t} + | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} val get_message : t -> string diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index fda4d7571..49774de3b 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -89,8 +89,8 @@ module C = struct let malloc access : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> - let astate = PulseOperations.allocate location access astate in + fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> + let astate = PulseOperations.allocate callee_procname location access astate in Ok [PulseOperations.write_id ret_id access astate] end @@ -245,6 +245,17 @@ module StdAtomicInteger = struct [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate] end +module ObjectiveC = struct + let alloc _ : model = + fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> + let hist = + [ValueHistory.Call {f= Model (Procname.to_string callee_procname); location; in_call= []}] + in + let ret_addr = AbstractValue.mk_fresh () in + let astate = PulseOperations.allocate callee_procname location (ret_addr, []) astate in + Ok [PulseOperations.write_id ret_id (ret_addr, hist) astate] +end + module JavaObject = struct (* naively modeled as shallow copy. *) let clone src_pointer_hist : model = @@ -513,7 +524,8 @@ module ProcNameDispatcher = struct ; ( +PatternMatch.implements_enumeration &:: "nextElement" <>$ capt_arg_payload $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) - ) ] + ) + ; +PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> ObjectiveC.alloc ] end let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d9bcdff89..e8aa64a52 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -374,7 +374,9 @@ let havoc_field location addr_trace field trace_obj astate = write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate -let allocate location addr_trace astate = AddressAttributes.allocate addr_trace location astate +let allocate procname location addr_trace astate = + AddressAttributes.allocate procname addr_trace location astate + let invalidate location cause addr_trace astate = check_addr_access location addr_trace astate @@ -474,17 +476,17 @@ let check_memory_leak_unreachable unreachable_attrs location = Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *)) ~f:(fun acc attr -> match (attr : Attribute.t) with - | Allocated trace -> - (Some trace, snd acc) + | Allocated (procname, trace) -> + (Some (procname, trace), snd acc) | Invalid (CFree, _) -> (fst acc, true) | _ -> acc ) in match allocated_not_freed_opt with - | Some trace, false -> + | Some (procname, trace), false -> (* allocated but not freed *) - Error (Diagnostic.MemoryLeak {location; allocation_trace= trace}) + Error (Diagnostic.MemoryLeak {procname; location; allocation_trace= trace}) | _ -> result in diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index b36e1e5d1..c3bd60c32 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -82,7 +82,7 @@ val invalidate : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** record that the address is invalid *) -val allocate : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t +val allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t val invalidate_deref : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result diff --git a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m new file mode 100644 index 000000000..cf41af741 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m @@ -0,0 +1,49 @@ +/* + * 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. + */ + +#import + +@interface MemoryLeaks + +@property(strong) UIView* backgroundCoveringView; +@property(strong) UIView* attachmentContainerView; + +@end + +@implementation MemoryLeaks + +- (void)cg_path_create_with_rect_no_leak_good_FP { + UIView* attachmentContainerView = [UIView alloc]; + CGPathRef shadowPath = + CGPathCreateWithRect(attachmentContainerView.bounds, NULL); + CGPathRelease(shadowPath); +} + +- (void)cg_path_create_with_rect_leak_bad { + CGPathRef shadowPath = + CGPathCreateWithRect(self.backgroundCoveringView.bounds, NULL); + self.backgroundCoveringView.layer.shadowPath = shadowPath; +} + ++ (void)cg_path_create_mutable_leak_bad:(CGRect)rect { + 0.20f * CGRectGetHeight(rect); + CGPathCreateMutable(); +} + ++ (void)cg_path_create_mutable_no_leak_good_FP:(CGRect)rect { + CGFloat lineThickness = 0.20f * CGRectGetHeight(rect); + // One rectangle + CGMutablePathRef path1 = CGPathCreateMutable(); + CFRelease(path1); +} + ++ (void)cg_bitmap_context_create_image_no_leak_good_FP { + CGImageRef newImage = CGBitmapContextCreateImage(nil); + CGImageRelease(newImage); +} + +@end diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 3acec4e7a..7b7cf2b98 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,2 +1,7 @@ +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_bitmap_context_create_image_no_leak_good_FP, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs 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,allocation occurs here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_mutable_no_leak_good_FP:, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_leak_bad, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_no_leak_good_FP, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]