diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 459acc30e..139ef7c06 100644 --- 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) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index c0f4ed090..73530e4d1 100644 --- 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. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 7b563052f..4af766eaf 100644 --- 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). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 217b9635c..7af2481de 100644 --- 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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 7037ed003..f94b91d20 100644 --- 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 diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 0f633a0b6..706023bfd 100644 --- 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 diff --git a/infer/tests/codetoanalyze/objc/pulse/Makefile b/infer/tests/codetoanalyze/objc/pulse/Makefile index 61da3acb8..3613c2f4b 100644 --- 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) diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index e7f29b7da..cb23bd5d5 100644 --- 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] diff --git a/infer/tests/codetoanalyze/objc/pulse/AllocPatternMemLeak.m b/infer/tests/codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm similarity index 69% rename from infer/tests/codetoanalyze/objc/pulse/AllocPatternMemLeak.m rename to infer/tests/codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm index d349ca4c5..e95005616 100644 --- a/infer/tests/codetoanalyze/objc/pulse/AllocPatternMemLeak.m +++ 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 diff --git a/infer/tests/codetoanalyze/objcpp/pulse/Makefile b/infer/tests/codetoanalyze/objcpp/pulse/Makefile index bb52b9734..bb7bed24d 100644 --- 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) diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index 76d89f920..fdc7e32ae 100644 --- 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]