From c76d59853b2ef46f6cf2d9989b421a9b8c25a637 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Wed, 22 Apr 2020 02:32:46 -0700 Subject: [PATCH] [pulse] Model CFBridgingRelease by removing the Allocated attribute Summary: `CFBridgingRelease` and `__bridge_transfer` which I'll model later, transfer the memory model from manual memory ref count to ARC (automatic ref count), so to avoid false positives this needs to be modelled. We can simply remove the Allocated attribute from the state, which means we won't try to track that memory anymore. Reviewed By: skcho Differential Revision: D21088218 fbshipit-source-id: 3520a0d59 --- infer/src/istd/PrettyPrintable.ml | 4 ++++ infer/src/istd/PrettyPrintable.mli | 2 ++ infer/src/pulse/PulseAbductiveDomain.ml | 4 ++++ infer/src/pulse/PulseAbductiveDomain.mli | 2 ++ infer/src/pulse/PulseAttribute.ml | 9 +++++++++ infer/src/pulse/PulseAttribute.mli | 2 ++ infer/src/pulse/PulseBaseAddressAttributes.ml | 17 +++++++++++++++++ infer/src/pulse/PulseBaseAddressAttributes.mli | 2 ++ infer/src/pulse/PulseModels.ml | 7 +++++++ infer/src/pulse/PulseOperations.ml | 2 ++ infer/src/pulse/PulseOperations.mli | 2 ++ infer/tests/codetoanalyze/objc/pulse/Makefile | 4 +++- .../codetoanalyze/objc/pulse/MemoryLeaks.m | 9 +++++++++ infer/tests/codetoanalyze/objc/pulse/issues.exp | 1 + 14 files changed, 66 insertions(+), 1 deletion(-) diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml index d0f4da0b6..27686a398 100644 --- a/infer/src/istd/PrettyPrintable.ml +++ b/infer/src/istd/PrettyPrintable.ml @@ -237,6 +237,8 @@ module type PPUniqRankSet = sig val singleton : elt -> t + val remove : elt -> t -> t + val union_prefer_left : t -> t -> t val pp : ?print_rank:bool -> F.formatter -> t -> unit @@ -295,6 +297,8 @@ module MakePPUniqRankSet (Val : PrintableRankedType) : PPUniqRankSet with type e else pp_collection ~pp_item:Val.pp fmt (Map.bindings map |> List.map ~f:snd) + let remove value map = Map.remove (Val.to_rank value) map + let singleton value = add Map.empty value let union_prefer_left m1 m2 = Map.union (fun _rank value1 _value2 -> Some value1) m1 m2 diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index 11d7f3989..27f3ac086 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/infer/src/istd/PrettyPrintable.mli @@ -188,6 +188,8 @@ module type PPUniqRankSet = sig val singleton : elt -> t + val remove : elt -> t -> t + val union_prefer_left : t -> t -> t (** in case an element with the same rank is present both in [lhs] and [rhs], keep the one from [lhs] in [union_prefer_left lhs rhs] *) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index db801840e..667c84c3b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -205,6 +205,10 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.allocate procname address location) + let remove_allocation_attr address astate = + map_post_attrs astate ~f:(BaseAddressAttributes.remove_allocation_attr address) + + let add_one address attributes astate = map_post_attrs astate ~f:(BaseAddressAttributes.add_one address attributes) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 3ab7bac8b..3cc540023 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -129,6 +129,8 @@ module AddressAttributes : sig val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t + val remove_allocation_attr : AbstractValue.t -> t -> t + val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option val is_std_vector_reserved : AbstractValue.t -> t -> bool diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 3041ab44b..501a40d41 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -67,6 +67,8 @@ module Attribute = struct let bo_itv_rank = Variants.to_rank (BoItv Itv.ItvPure.zero) + let allocated_rank = Variants.to_rank (Allocated (Procname.Linters_dummy_method, dummy_trace)) + let pp f attribute = let pp_string_if_debug string fmt = if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string @@ -146,6 +148,13 @@ module Attributes = struct || Option.is_some (Set.find_rank attrs Attribute.invalid_rank) + let get_allocation attrs = + Set.find_rank attrs Attribute.allocated_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.Allocated (procname, trace)) = attr in + (procname, trace) ) + + let get_citv attrs = Set.find_rank attrs Attribute.const_rank |> Option.map ~f:(fun attr -> diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 81772068b..4a57d692c 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -39,6 +39,8 @@ module Attributes : sig val get_closure_proc_name : t -> Procname.t option + val get_allocation : t -> (Procname.t * Trace.t) option + val get_citv : t -> (CItv.t * Trace.t) option val get_bo_itv : t -> Itv.ItvPure.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index b9c34b77e..b5fc4e0cf 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -28,6 +28,15 @@ let add_one addr attribute attrs = Graph.add addr new_attrs attrs +let remove_one addr attribute attrs = + match Graph.find_opt addr attrs with + | None -> + attrs + | Some old_attrs -> + let new_attrs = Attributes.remove attribute old_attrs in + Graph.add addr new_attrs attrs + + let add addr attributes attrs = match Graph.find_opt addr attrs with | None -> @@ -71,6 +80,14 @@ let get_attribute getter address attrs = Graph.find_opt address attrs >>= getter +let remove_allocation_attr address memory = + match get_attribute Attributes.get_allocation address memory with + | Some (procname, trace) -> + remove_one address (Attribute.Allocated (procname, trace)) memory + | None -> + memory + + let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name let get_citv = get_attribute Attributes.get_citv diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 1bddc14ed..1a3a46cac 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -43,3 +43,5 @@ val std_vector_reserve : AbstractValue.t -> t -> t val is_std_vector_reserved : AbstractValue.t -> t -> bool val pp : F.formatter -> t -> unit + +val remove_allocation_attr : AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 3e6ddeca1..4dbf4cd00 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -116,6 +116,12 @@ module C = struct PulseOperations.allocate callee_procname location ret_value astate |> PulseArithmetic.and_positive immediate_hist ret_addr |> PulseOperations.ok_continue + + + let cf_bridging_release access : model = + fun ~caller_summary:_ ~callee_procname:_ _ ~ret:(ret_id, _) astate -> + let astate = PulseOperations.write_id ret_id access astate in + PulseOperations.remove_allocation_attr (fst access) astate |> PulseOperations.ok_continue end module Cplusplus = struct @@ -649,6 +655,7 @@ module ProcNameDispatcher = struct ; +PatternMatch.ObjectiveC.is_core_graphics_release <>$ capt_arg_payload $--> C.free ; -"CFRelease" <>$ capt_arg_payload $--> C.free ; -"CFAutorelease" <>$ capt_arg_payload $--> C.free + ; -"CFBridgingRelease" <>$ capt_arg_payload $--> C.cf_bridging_release ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null ; +PatternMatch.ObjectiveC.is_modelled_as_free <>$ capt_arg_payload $--> C.free ] end diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index e755907e6..49a603a1c 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -225,6 +225,8 @@ let allocate procname location addr_trace astate = AddressAttributes.allocate procname addr_trace location astate +let remove_allocation_attr address astate = AddressAttributes.remove_allocation_attr address astate + let invalidate location cause addr_trace astate = check_addr_access location addr_trace astate >>| AddressAttributes.invalidate addr_trace cause location diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index ec9f6f225..dcf77d612 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -84,6 +84,8 @@ val invalidate : val allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t +val remove_allocation_attr : AbstractValue.t -> t -> t + val invalidate_deref : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** record that what the address points to is invalid *) diff --git a/infer/tests/codetoanalyze/objc/pulse/Makefile b/infer/tests/codetoanalyze/objc/pulse/Makefile index ebe0588bf..18b58cb7f 100644 --- a/infer/tests/codetoanalyze/objc/pulse/Makefile +++ b/infer/tests/codetoanalyze/objc/pulse/Makefile @@ -6,7 +6,9 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS) -INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) --pulse-model-alloc-pattern AB[IF].*Create.* --pulse-model-free-pattern ABFRelease +INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \ +--pulse-model-alloc-pattern "AB[IF].*Create.*\|CFLocaleCreate" \ +--pulse-model-free-pattern ABFRelease INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.m) diff --git a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m index 87b99d5bc..7706e754a 100644 --- a/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m +++ b/infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m @@ -53,4 +53,13 @@ CFAutorelease(newImage); } +- (void)bridge_no_leak_good { + CFLocaleRef nameRef = CFLocaleCreate(NULL, NULL); + NSLocale* a = CFBridgingRelease(nameRef); +} + +- (void)no_bridge_leak_bad { + CFLocaleRef nameRef = CFLocaleCreate(NULL, NULL); +} + @end diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 51e84d8db..aa6c9bdb3 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,5 +1,6 @@ codetoanalyze/objc/pulse/AllocPatternMemLeak.m, A::create_no_release_leak_bad, 1, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `ABFDataCreate` (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] 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,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::no_bridge_leak_bad, 1, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CFLocaleCreate` (modelled),allocation part of the trace ends 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]