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]