[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

@@ -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

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] *)

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)
 

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

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 ->

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

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

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

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

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

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 *)

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)

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

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]