[pulse] Add a flag to model methods for memory ownership transfer

Summary: Just like `CFBridgingRelease` we want to be able to model functions that are specific to a given codebase that make a transfer of memory ownership so that developers don't need to worry about releasing that memory anymore, and hence, we don't want to report leaks on that memory. Things get a little more complicated, because some of the functions we want to model are in a specific namespace, so with this flag we take both cases into account, when we are dealing with namespaces or not. Reviewed By: jvillard Differential Revision: D21404409 fbshipit-source-id: c36bd7afc
5 years ago · ef7bc324e3
parent aad4f581e8
commit ef7bc324e3
11 changed files with 246 additions and 160 deletions
--- a/infer/man/man1/infer-analyze.txt
+++ b/infer/man/man1/infer-analyze.txt
@ -243,6 +243,10 @@ OPTIONS
       --pulse-model-release-pattern string
           Regex of methods that should be modelled as release in Pulse

+       --pulse-model-transfer-ownership +string
+           Methods that should be modelled as transfering memory ownership in
+           Pulse. Accepted formats are method or namespace::method
+
       --pulse-only
           Activates: Enable --pulse and disable all other checkers
           (Conversely: --no-pulse-only)
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@ -870,6 +870,11 @@ OPTIONS
           Regex of methods that should be modelled as release in Pulse       
    See also infer-analyze(1).

+       --pulse-model-transfer-ownership +string
+           Methods that should be modelled as transfering memory ownership in
+           Pulse. Accepted formats are method or namespace::method       
+    See also infer-analyze(1).
+
       --pulse-only
           Activates: Enable --pulse and disable all other checkers
           (Conversely: --no-pulse-only)           See also infer-analyze(1).
@ -1616,6 +1621,9 @@ INTERNAL OPTIONS
       --pulse-model-release-pattern-reset
           Cancel the effect of --pulse-model-release-pattern.

+       --pulse-model-transfer-ownership-reset
+           Set --pulse-model-transfer-ownership to the empty list.
+
       --pulse-recency-limit int
           Maximum number of array elements and structure fields to keep
           track of for a given array address.
--- a/infer/man/man1/infer.txt
+++ b/infer/man/man1/infer.txt
@ -870,6 +870,11 @@ OPTIONS
           Regex of methods that should be modelled as release in Pulse       
    See also infer-analyze(1).

+       --pulse-model-transfer-ownership +string
+           Methods that should be modelled as transfering memory ownership in
+           Pulse. Accepted formats are method or namespace::method       
+    See also infer-analyze(1).
+
       --pulse-only
           Activates: Enable --pulse and disable all other checkers
           (Conversely: --no-pulse-only)           See also infer-analyze(1).
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@ -1788,6 +1788,13 @@ and pulse_model_release_pattern =
    "Regex of methods that should be modelled as release in Pulse"


+and pulse_model_transfer_ownership =
+  CLOpt.mk_string_list ~long:"pulse-model-transfer-ownership"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "Methods that should be modelled as transfering memory ownership in Pulse. Accepted formats \
+     are method or namespace::method"
+
+
 and pulse_widen_threshold =
  CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3
    "Under-approximate after $(i,int) loop iterations"
@ -2868,6 +2875,27 @@ and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_patt

 and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern

+and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
+  let models =
+    let re = Str.regexp "::" in
+    List.map ~f:(fun model -> (model, Str.split re model)) !pulse_model_transfer_ownership
+  in
+  let aux el =
+    match el with
+    | _, [namespace; m] ->
+        `Fst (namespace, m)
+    | _, [m] ->
+        `Snd m
+    | option, splits ->
+        L.die UserError
+          "Wrong use of option pulse-model-transfer-ownership %s: expected at most one namespace \
+           but found %d"
+          option
+          (List.length splits - 1)
+  in
+  List.partition_map ~f:aux models
+
+
 and pulse_widen_threshold = !pulse_widen_threshold

 and pure_by_default = !pure_by_default
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@ -457,6 +457,10 @@ val pulse_model_alloc_pattern : Str.regexp option

 val pulse_model_release_pattern : Str.regexp option

+val pulse_model_transfer_ownership_namespace : (string * string) list
+
+val pulse_model_transfer_ownership : string list
+
 val pulse_widen_threshold : int

 val pure_by_default : bool
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@ -108,8 +108,9 @@ module C = struct
    PulseOperations.allocate callee_procname location ret_value astate
    |> PulseArithmetic.and_positive ret_addr
    |> PulseOperations.ok_continue
+end

-
+module ObjCCoreFoundation = struct
  let cf_bridging_release access : model =
   fun _ ~callee_procname:_ _ ~ret:(ret_id, _) astate ->
    let astate = PulseOperations.write_id ret_id access astate in
@ -622,160 +623,179 @@ module ProcNameDispatcher = struct
      StringSet.of_list
        ["add"; "addAll"; "append"; "delete"; "remove"; "replace"; "poll"; "put"; "putAll"]
    in
+    let transfer_ownership_matchers =
+      let transfer_ownership_namespace_matchers =
+        List.map
+          ~f:(fun (namespace, m) ->
+            -namespace &:: m $ capt_arg_payload $+...$--> ObjCCoreFoundation.cf_bridging_release )
+          Config.pulse_model_transfer_ownership_namespace
+      in
+      let transfer_ownership_name_matchers =
+        List.map
+          ~f:(fun m -> -m $ capt_arg_payload $+...$--> ObjCCoreFoundation.cf_bridging_release)
+          Config.pulse_model_transfer_ownership
+      in
+      transfer_ownership_namespace_matchers @ transfer_ownership_name_matchers
+    in
    make_dispatcher
-      [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
-      ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
-      ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
-      ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
-      ; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit
-      ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg
-      ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit
-      ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
-      ; +match_builtin BuiltinDecl.__infer_initializer_list
-        <>$ capt_arg_payload $+...$--> Misc.id_first_arg
-      ; +PatternMatch.implements_lang "System" &:: "exit" <>--> Misc.early_exit
-      ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size
-      ; (* consider that all fbstrings are small strings to avoid false positives due to manual
-           ref-counting *)
-        -"folly" &:: "fbstring_core" &:: "category" &--> Misc.return_int Int64.zero
-      ; -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip
-      ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip
-      ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip
-      ; -"std" &:: "basic_string" &:: "data" <>$ capt_arg_payload $--> StdBasicString.data
-      ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_arg_payload
-        $--> StdBasicString.destructor
-      ; -"std" &:: "function" &:: "operator()" $ capt_arg_payload $++$--> StdFunction.operator_call
-      ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload
-        $--> Misc.shallow_copy "std::function::operator="
-      ; +PatternMatch.implements_lang "Object" &:: "clone" $ capt_arg_payload $--> JavaObject.clone
-      ; ( +PatternMatch.implements_lang "System"
-        &:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload
-        $+...$--> fun src dest -> Misc.shallow_copy "System.arraycopy" dest src )
-      ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdAtomicInteger.constructor
-      ; -"std" &:: "__atomic_base" &:: "fetch_add" <>$ capt_arg_payload $+ capt_arg_payload
-        $+ capt_arg_payload $--> StdAtomicInteger.fetch_add
-      ; -"std" &:: "__atomic_base" &:: "fetch_sub" <>$ capt_arg_payload $+ capt_arg_payload
-        $+ capt_arg_payload $--> StdAtomicInteger.fetch_sub
-      ; -"std" &:: "__atomic_base" &:: "exchange" <>$ capt_arg_payload $+ capt_arg_payload
-        $+ capt_arg_payload $--> StdAtomicInteger.exchange
-      ; -"std" &:: "__atomic_base" &:: "load" <>$ capt_arg_payload $+? capt_arg_payload
-        $--> StdAtomicInteger.load
-      ; -"std" &:: "__atomic_base" &:: "store" <>$ capt_arg_payload $+ capt_arg_payload
-        $+ capt_arg_payload $--> StdAtomicInteger.store
-      ; -"std" &:: "__atomic_base" &:: "operator++" <>$ capt_arg_payload
-        $--> StdAtomicInteger.operator_plus_plus_pre
-      ; -"std" &:: "__atomic_base" &:: "operator++" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdAtomicInteger.operator_plus_plus_post
-      ; -"std" &:: "__atomic_base" &:: "operator--" <>$ capt_arg_payload
-        $--> StdAtomicInteger.operator_minus_minus_pre
-      ; -"std" &:: "__atomic_base" &:: "operator--" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdAtomicInteger.operator_minus_minus_post
-      ; -"std" &:: "__atomic_base"
-        &::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
-        <>$ capt_arg_payload $+? capt_arg_payload $--> StdAtomicInteger.operator_t
-      ; -"std" &:: "integral_constant" < any_typ &+ capt_int
-        >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
-        <>--> Misc.return_int
-      ; -"std" &:: "vector" &:: "vector" <>$ capt_arg_payload
-        $+ capt_arg_payload_of_typ (-"std" &:: "initializer_list")
-        $+...$--> StdVector.init_list_constructor
-      ; -"std" &:: "__wrap_iter" &:: "__wrap_iter" <>$ capt_arg_payload $+ capt_arg_payload
-        $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
-      ; -"std" &:: "__wrap_iter" &:: "operator*" <>$ capt_arg_payload
-        $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*"
-      ; -"std" &:: "__wrap_iter" &:: "operator++" <>$ capt_arg_payload
-        $--> GenericArrayBackedCollectionIterator.operator_step `PlusPlus
-               ~desc:"iterator operator++"
-      ; -"std" &:: "__wrap_iter" &:: "operator--" <>$ capt_arg_payload
-        $--> GenericArrayBackedCollectionIterator.operator_step `MinusMinus
-               ~desc:"iterator operator--"
-      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "__normal_iterator" <>$ capt_arg_payload
-        $+ capt_arg_payload
-        $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
-      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator*" <>$ capt_arg_payload
-        $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*"
-      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator++" <>$ capt_arg_payload
-        $--> GenericArrayBackedCollectionIterator.operator_step `PlusPlus
-               ~desc:"iterator operator++"
-      ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator--" <>$ capt_arg_payload
-        $--> GenericArrayBackedCollectionIterator.operator_step `MinusMinus
-               ~desc:"iterator operator--"
-      ; -"std" &:: "vector" &:: "assign" <>$ capt_arg_payload
-        $+...$--> StdVector.invalidate_references Assign
-      ; -"std" &:: "vector" &:: "at" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdVector.at ~desc:"std::vector::at()"
-      ; -"std" &:: "vector" &:: "begin" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdVector.vector_begin
-      ; -"std" &:: "vector" &:: "end" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdVector.vector_end
-      ; -"std" &:: "vector" &:: "clear" <>$ capt_arg_payload
-        $--> StdVector.invalidate_references Clear
-      ; -"std" &:: "vector" &:: "emplace" $ capt_arg_payload
-        $+...$--> StdVector.invalidate_references Emplace
-      ; -"std" &:: "vector" &:: "emplace_back" $ capt_arg_payload
-        $+...$--> StdVector.invalidate_references EmplaceBack
-      ; -"std" &:: "vector" &:: "insert" <>$ capt_arg_payload
-        $+...$--> StdVector.invalidate_references Insert
-      ; -"std" &:: "vector" &:: "operator[]" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdVector.at ~desc:"std::vector::at()"
-      ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload
-        $--> StdVector.invalidate_references ShrinkToFit
-      ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; +PatternMatch.implements_collection
-        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
-        <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; +PatternMatch.implements_queue
-        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
-        <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; +PatternMatch.implements_lang "StringBuilder"
-        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
-        <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; +PatternMatch.implements_lang "StringBuilder"
-        &:: "setLength" <>$ capt_arg_payload
-        $+...$--> StdVector.invalidate_references ShrinkToFit
-      ; +PatternMatch.implements_lang "String"
-        &::+ (fun _ str -> StringSet.mem str pushback_modeled)
-        <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload
-        $+...$--> JavaIterator.remove ~desc:"remove"
-      ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; +PatternMatch.implements_map &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back
-      ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
-      ; +PatternMatch.implements_collection
-        &:: "get" <>$ capt_arg_payload $+ capt_arg_payload
-        $--> StdVector.at ~desc:"Collection.get()"
-      ; +PatternMatch.implements_list &:: "set" <>$ capt_arg_payload $+ capt_arg_payload
-        $+ capt_arg_payload $--> JavaCollection.set
-      ; +PatternMatch.implements_iterator &:: "hasNext"
-        &--> Misc.nondet ~fn_name:"Iterator.hasNext()"
-      ; +PatternMatch.implements_enumeration
-        &:: "hasMoreElements"
-        &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()"
-      ; +PatternMatch.implements_lang "Object"
-        &:: "equals"
-        &--> Misc.nondet ~fn_name:"Object.equals"
-      ; +PatternMatch.implements_lang "Iterable"
-        &:: "iterator" <>$ capt_arg_payload
-        $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator"
-      ; +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload
-        $!--> JavaIterator.next ~desc:"Iterator.next()"
-      ; ( +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 &++> C.malloc
-      ; +PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc
-      ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_arg_payload $--> C.malloc_not_null
-      ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null
-      ; +PatternMatch.ObjectiveC.is_core_graphics_release
-        <>$ capt_arg_payload $--> C.cf_bridging_release
-      ; -"CFRelease" <>$ capt_arg_payload $--> C.cf_bridging_release
-      ; +PatternMatch.ObjectiveC.is_modelled_as_release
-        <>$ capt_arg_payload $--> C.cf_bridging_release
-      ; -"CFAutorelease" <>$ capt_arg_payload $--> C.cf_bridging_release
-      ; -"CFBridgingRelease" <>$ capt_arg_payload $--> C.cf_bridging_release
-      ; +match_builtin BuiltinDecl.__free_cf <>$ capt_arg_payload $--> C.cf_bridging_release ]
+      ( transfer_ownership_matchers
+      @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
+        ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
+        ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
+        ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
+        ; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit
+        ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg
+        ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit
+        ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit
+        ; +match_builtin BuiltinDecl.__infer_initializer_list
+          <>$ capt_arg_payload $+...$--> Misc.id_first_arg
+        ; +PatternMatch.implements_lang "System" &:: "exit" <>--> Misc.early_exit
+        ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size
+        ; (* consider that all fbstrings are small strings to avoid false positives due to manual
+             ref-counting *)
+          -"folly" &:: "fbstring_core" &:: "category" &--> Misc.return_int Int64.zero
+        ; -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip
+        ; -"folly" &:: "Optional" &:: "reset" &--> Misc.skip
+        ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip
+        ; -"std" &:: "basic_string" &:: "data" <>$ capt_arg_payload $--> StdBasicString.data
+        ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_arg_payload
+          $--> StdBasicString.destructor
+        ; -"std" &:: "function" &:: "operator()" $ capt_arg_payload
+          $++$--> StdFunction.operator_call
+        ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload
+          $--> Misc.shallow_copy "std::function::operator="
+        ; +PatternMatch.implements_lang "Object"
+          &:: "clone" $ capt_arg_payload $--> JavaObject.clone
+        ; ( +PatternMatch.implements_lang "System"
+          &:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload
+          $+...$--> fun src dest -> Misc.shallow_copy "System.arraycopy" dest src )
+        ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdAtomicInteger.constructor
+        ; -"std" &:: "__atomic_base" &:: "fetch_add" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ capt_arg_payload $--> StdAtomicInteger.fetch_add
+        ; -"std" &:: "__atomic_base" &:: "fetch_sub" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ capt_arg_payload $--> StdAtomicInteger.fetch_sub
+        ; -"std" &:: "__atomic_base" &:: "exchange" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ capt_arg_payload $--> StdAtomicInteger.exchange
+        ; -"std" &:: "__atomic_base" &:: "load" <>$ capt_arg_payload $+? capt_arg_payload
+          $--> StdAtomicInteger.load
+        ; -"std" &:: "__atomic_base" &:: "store" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ capt_arg_payload $--> StdAtomicInteger.store
+        ; -"std" &:: "__atomic_base" &:: "operator++" <>$ capt_arg_payload
+          $--> StdAtomicInteger.operator_plus_plus_pre
+        ; -"std" &:: "__atomic_base" &:: "operator++" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdAtomicInteger.operator_plus_plus_post
+        ; -"std" &:: "__atomic_base" &:: "operator--" <>$ capt_arg_payload
+          $--> StdAtomicInteger.operator_minus_minus_pre
+        ; -"std" &:: "__atomic_base" &:: "operator--" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdAtomicInteger.operator_minus_minus_post
+        ; -"std" &:: "__atomic_base"
+          &::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
+          <>$ capt_arg_payload $+? capt_arg_payload $--> StdAtomicInteger.operator_t
+        ; -"std" &:: "integral_constant" < any_typ &+ capt_int
+          >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name)
+          <>--> Misc.return_int
+        ; -"std" &:: "vector" &:: "vector" <>$ capt_arg_payload
+          $+ capt_arg_payload_of_typ (-"std" &:: "initializer_list")
+          $+...$--> StdVector.init_list_constructor
+        ; -"std" &:: "__wrap_iter" &:: "__wrap_iter" <>$ capt_arg_payload $+ capt_arg_payload
+          $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
+        ; -"std" &:: "__wrap_iter" &:: "operator*" <>$ capt_arg_payload
+          $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*"
+        ; -"std" &:: "__wrap_iter" &:: "operator++" <>$ capt_arg_payload
+          $--> GenericArrayBackedCollectionIterator.operator_step `PlusPlus
+                 ~desc:"iterator operator++"
+        ; -"std" &:: "__wrap_iter" &:: "operator--" <>$ capt_arg_payload
+          $--> GenericArrayBackedCollectionIterator.operator_step `MinusMinus
+                 ~desc:"iterator operator--"
+        ; -"__gnu_cxx" &:: "__normal_iterator" &:: "__normal_iterator" <>$ capt_arg_payload
+          $+ capt_arg_payload
+          $+...$--> GenericArrayBackedCollectionIterator.constructor ~desc:"iterator constructor"
+        ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator*" <>$ capt_arg_payload
+          $--> GenericArrayBackedCollectionIterator.operator_star ~desc:"iterator operator*"
+        ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator++" <>$ capt_arg_payload
+          $--> GenericArrayBackedCollectionIterator.operator_step `PlusPlus
+                 ~desc:"iterator operator++"
+        ; -"__gnu_cxx" &:: "__normal_iterator" &:: "operator--" <>$ capt_arg_payload
+          $--> GenericArrayBackedCollectionIterator.operator_step `MinusMinus
+                 ~desc:"iterator operator--"
+        ; -"std" &:: "vector" &:: "assign" <>$ capt_arg_payload
+          $+...$--> StdVector.invalidate_references Assign
+        ; -"std" &:: "vector" &:: "at" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdVector.at ~desc:"std::vector::at()"
+        ; -"std" &:: "vector" &:: "begin" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdVector.vector_begin
+        ; -"std" &:: "vector" &:: "end" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdVector.vector_end
+        ; -"std" &:: "vector" &:: "clear" <>$ capt_arg_payload
+          $--> StdVector.invalidate_references Clear
+        ; -"std" &:: "vector" &:: "emplace" $ capt_arg_payload
+          $+...$--> StdVector.invalidate_references Emplace
+        ; -"std" &:: "vector" &:: "emplace_back" $ capt_arg_payload
+          $+...$--> StdVector.invalidate_references EmplaceBack
+        ; -"std" &:: "vector" &:: "insert" <>$ capt_arg_payload
+          $+...$--> StdVector.invalidate_references Insert
+        ; -"std" &:: "vector" &:: "operator[]" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdVector.at ~desc:"std::vector::at()"
+        ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload
+          $--> StdVector.invalidate_references ShrinkToFit
+        ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_collection
+          &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+          <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_queue
+          &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+          <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_lang "StringBuilder"
+          &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+          <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_lang "StringBuilder"
+          &:: "setLength" <>$ capt_arg_payload
+          $+...$--> StdVector.invalidate_references ShrinkToFit
+        ; +PatternMatch.implements_lang "String"
+          &::+ (fun _ str -> StringSet.mem str pushback_modeled)
+          <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload
+          $+...$--> JavaIterator.remove ~desc:"remove"
+        ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back
+        ; +PatternMatch.implements_map &:: "putAll" <>$ capt_arg_payload
+          $+...$--> StdVector.push_back
+        ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve
+        ; +PatternMatch.implements_collection
+          &:: "get" <>$ capt_arg_payload $+ capt_arg_payload
+          $--> StdVector.at ~desc:"Collection.get()"
+        ; +PatternMatch.implements_list &:: "set" <>$ capt_arg_payload $+ capt_arg_payload
+          $+ capt_arg_payload $--> JavaCollection.set
+        ; +PatternMatch.implements_iterator &:: "hasNext"
+          &--> Misc.nondet ~fn_name:"Iterator.hasNext()"
+        ; +PatternMatch.implements_enumeration
+          &:: "hasMoreElements"
+          &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()"
+        ; +PatternMatch.implements_lang "Object"
+          &:: "equals"
+          &--> Misc.nondet ~fn_name:"Object.equals"
+        ; +PatternMatch.implements_lang "Iterable"
+          &:: "iterator" <>$ capt_arg_payload
+          $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator"
+        ; +PatternMatch.implements_iterator &:: "next" <>$ capt_arg_payload
+          $!--> JavaIterator.next ~desc:"Iterator.next()"
+        ; ( +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 &++> C.malloc
+        ; +PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc
+        ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_arg_payload $--> C.malloc_not_null
+        ; +PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null
+        ; +PatternMatch.ObjectiveC.is_core_graphics_release
+          <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
+        ; -"CFRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
+        ; +PatternMatch.ObjectiveC.is_modelled_as_release
+          <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
+        ; -"CFAutorelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
+        ; -"CFBridgingRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
+        ; +match_builtin BuiltinDecl.__free_cf
+          <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ] )
 end

 let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args
--- a/infer/tests/codetoanalyze/objc/pulse/Makefile
+++ b/infer/tests/codetoanalyze/objc/pulse/Makefile
@ -6,9 +6,7 @@
 TESTS_DIR = ../../..

 CLANG_OPTIONS = -c $(OBJC_CLANG_OPTIONS) -fobjc-arc
-INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
--pulse-model-alloc-pattern "AB[IF].*Create.*" \
--pulse-model-release-pattern ABFRelease
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
 INFERPRINT_OPTIONS = --issues-tests

 SOURCES = $(wildcard *.m)
--- a/infer/tests/codetoanalyze/objc/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp
@ -1,4 +1,3 @@
-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/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]
--- a/infer/tests/codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm
+++ b/infer/tests/codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm
@ -16,6 +16,12 @@ typedef struct ABFDataRef {
 ABFDataRef* ABFDataCreate(size_t size);
 void ABFRelease(ABFDataRef*);

+ABFData* ABFBridgingRelease(ABFDataRef*);
+
+namespace abf {
+ABFData* BridgingRelease(ABFDataRef*);
+}
+
@interface A : NSObject
@end

@ -34,4 +40,12 @@ void ABFRelease(ABFDataRef*);
  ABFData* someData = (__bridge_transfer ABFData*)ABFDataCreate(4);
 }

+- (void)custom_bridge_no_leak_good {
+  ABFData* someData = ABFBridgingRelease(ABFDataCreate(4));
+}
+
+- (void)custom_bridge_namesapce_no_leak_good {
+  ABFData* someData = abf::BridgingRelease(ABFDataCreate(4));
+}
+
@end
--- a/infer/tests/codetoanalyze/objcpp/pulse/Makefile
+++ b/infer/tests/codetoanalyze/objcpp/pulse/Makefile
@ -5,8 +5,13 @@

 TESTS_DIR = ../../..

-CLANG_OPTIONS = -c $(OBJCPP_CLANG_OPTIONS)
-INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
+CLANG_OPTIONS = -c $(OBJCPP_CLANG_OPTIONS) -fobjc-arc
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
+--pulse-model-alloc-pattern "AB[IF].*Create.*" \
+--pulse-model-release-pattern "ABFRelease" \
+--pulse-model-transfer-ownership "abf::BridgingRelease" \
+--pulse-model-transfer-ownership "ABFBridgingRelease"
+
 INFERPRINT_OPTIONS = --issues-tests

 SOURCES = $(wildcard *.mm)
--- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp
@ -1,2 +1,3 @@
+codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, 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/objcpp/pulse/use_after_delete.mm, PulseTest::deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]