diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index c21966e1a..60a104f8f 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -261,6 +261,9 @@ OPTIONS --pulse-model-return-nonnull +string Methods that should be modelled as returning non-null in Pulse + --pulse-model-skip-pattern string + Regex of methods that should be modelled as "skip" 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 diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 2f8e5116c..9287bfbc6 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -920,6 +920,10 @@ OPTIONS Methods that should be modelled as returning non-null in Pulse See also infer-analyze(1). + --pulse-model-skip-pattern string + Regex of methods that should be modelled as "skip" 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 @@ -1724,6 +1728,9 @@ INTERNAL OPTIONS --pulse-model-return-nonnull-reset Set --pulse-model-return-nonnull to the empty list. + --pulse-model-skip-pattern-reset + Cancel the effect of --pulse-model-skip-pattern. + --pulse-model-transfer-ownership-reset Set --pulse-model-transfer-ownership to the empty list. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index c0f49646c..4f2c1a40e 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -920,6 +920,10 @@ OPTIONS Methods that should be modelled as returning non-null in Pulse See also infer-analyze(1). + --pulse-model-skip-pattern string + Regex of methods that should be modelled as "skip" 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 diff --git a/infer/src/absint/ProcnameDispatcher.ml b/infer/src/absint/ProcnameDispatcher.ml index 4f49b342a..506e60d57 100644 --- a/infer/src/absint/ProcnameDispatcher.ml +++ b/infer/src/absint/ProcnameDispatcher.ml @@ -852,6 +852,8 @@ module Call = struct let ( &::.*--> ) name_matcher f = name_matcher <...>! () &::.*! () $! () $+...$--> f + let ( &::.*++> ) name_matcher f = name_matcher <...>! () &::.*! () $! () $++$--> f + let ( $!--> ) args_matcher f = args_matcher $* exact_args_or_retry wrong_args_internal_error $*--> f end diff --git a/infer/src/absint/ProcnameDispatcher.mli b/infer/src/absint/ProcnameDispatcher.mli index 6a265a21d..04259a44d 100644 --- a/infer/src/absint/ProcnameDispatcher.mli +++ b/infer/src/absint/ProcnameDispatcher.mli @@ -139,7 +139,6 @@ module type NameCommon = sig ('context, 'f_in, 'f_out, 'arg_payload) name_matcher -> 'f_in -> ('context, 'f_out, 'arg_payload) matcher - (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates), accepts ALL function arguments, binds the function *) end @@ -324,6 +323,13 @@ module Call : sig (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates), accepts ALL function arguments, binds the function *) + val ( &::.*++> ) : + ('context, 'f_in, 'arg_payload FuncArg.t list -> 'f_out, 'arg_payload) name_matcher + -> 'f_in + -> ('context, 'f_out, 'arg_payload) matcher + (** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates), + captures ALL function arguments as a list, binds the function *) + val ( $!--> ) : ('context, 'f_in, 'f_proc_out, 'f_out, 'arg_payload) args_matcher -> 'f_in diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index fc016be75..ec572b5e7 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1874,6 +1874,12 @@ and pulse_model_return_nonnull = "Methods that should be modelled as returning non-null in Pulse" +and pulse_model_skip_pattern = + CLOpt.mk_string_opt ~long:"pulse-model-skip-pattern" + ~in_help:InferCommand.[(Analyze, manual_generic)] + "Regex of methods that should be modelled as \"skip\" in Pulse" + + and pulse_model_transfer_ownership = CLOpt.mk_string_list ~long:"pulse-model-transfer-ownership" ~in_help:InferCommand.[(Analyze, manual_generic)] @@ -3002,6 +3008,8 @@ and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_ and pulse_model_return_nonnull = !pulse_model_return_nonnull +and pulse_model_skip_pattern = Option.map ~f:Str.regexp !pulse_model_skip_pattern + and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership = let models = let re = Str.regexp "::" in diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index ed9ac3c12..4203bd309 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -463,6 +463,8 @@ val pulse_model_release_pattern : Str.regexp option val pulse_model_return_nonnull : string list +val pulse_model_skip_pattern : Str.regexp option + val pulse_model_transfer_ownership_namespace : (string * string) list val pulse_model_transfer_ownership : string list diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 343b21725..837fc9816 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -74,7 +74,28 @@ module Misc = struct PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue - let skip : model = fun _ ~callee_procname:_ _ ~ret:_ astate -> PulseOperations.ok_continue astate + (** Pretend the function call is a call to an "unknown" function, i.e. a function for which we + don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we + suspect are passed by reference. *) + let unknown_call skip_reason args : model = + fun _ ~callee_procname location ~ret astate -> + let actuals = + List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} -> + (actual, typ) ) + in + let formals_opt = + AnalysisCallbacks.proc_resolve_attributes callee_procname + |> Option.map ~f:ProcAttributes.get_pvar_formals + in + Ok + [ ExecutionDomain.ContinueProgram + (PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt + astate) ] + + + (** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a + good idea) *) + let skip = unknown_call let nondet ~fn_name : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> @@ -819,7 +840,7 @@ end module StringSet = Caml.Set.Make (String) module ProcNameDispatcher = struct - let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher = + let dispatch : (Tenv.t * Procname.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in let match_builtin builtin _ s = String.equal s (Procname.get_method builtin) in let pushback_modeled = @@ -859,6 +880,13 @@ module ProcNameDispatcher = struct ~model:(fun m -> Misc.return_positive ~desc:m) Config.pulse_model_return_nonnull in + let match_regexp_opt r_opt (_tenv, proc_name) _ = + Option.value_map ~default:false r_opt ~f:(fun r -> + let s = Procname.to_string proc_name in + let r = Str.string_match r s 0 in + r ) + in + let map_context_tenv f (x, _) = f x in make_dispatcher ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free @@ -872,13 +900,16 @@ module ProcNameDispatcher = struct ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit ; +match_builtin BuiltinDecl.__infer_initializer_list <>$ capt_arg_payload $+...$--> Misc.id_first_arg - ; +PatternMatch.Java.implements_lang "System" &:: "exit" <>--> Misc.early_exit + ; +map_context_tenv (PatternMatch.Java.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" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip + ; -"folly" &:: "DelayedDestruction" &:: "destroy" + &++> Misc.skip "folly::DelayedDestruction::destroy is modelled as skip" + ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" + &++> Misc.skip "folly::SocketAddress's destructor is modelled as skip" ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload $+ any_arg_of_typ (-"folly" &:: "None") $--> FollyOptional.assign_none ~desc:"folly::Optional::Optional(=None)" @@ -906,11 +937,11 @@ module ProcNameDispatcher = struct ; -"std" &:: "function" &:: "operator()" $ capt_arg $++$--> StdFunction.operator_call ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg $--> StdFunction.assign ~desc:"std::function::operator=" - ; +PatternMatch.Java.implements_lang "Object" + ; +map_context_tenv (PatternMatch.Java.implements_lang "Object") &:: "clone" $ capt_arg_payload $--> JavaObject.clone - ; ( +PatternMatch.Java.implements_lang "System" + ; +map_context_tenv (PatternMatch.Java.implements_lang "System") &:: "arraycopy" $ capt_arg_payload $+ any_arg $+ capt_arg_payload - $+...$--> fun src dest -> Misc.shallow_copy_model "System.arraycopy" dest src ) + $+...$--> (fun src dest -> Misc.shallow_copy_model "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 @@ -1002,79 +1033,81 @@ module ProcNameDispatcher = struct ; -"std" &:: "vector" &:: "shrink_to_fit" <>$ capt_arg_payload $--> StdVector.invalidate_references ShrinkToFit ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back - ; +PatternMatch.Java.implements_collection + ; +map_context_tenv PatternMatch.Java.implements_collection &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add - ; +PatternMatch.Java.implements_list + ; +map_context_tenv PatternMatch.Java.implements_list &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add_at - ; +PatternMatch.Java.implements_collection + ; +map_context_tenv PatternMatch.Java.implements_collection &:: "remove" <>$ capt_arg_payload $+ any_arg $--> JavaCollection.remove - ; +PatternMatch.Java.implements_list + ; +map_context_tenv PatternMatch.Java.implements_list &:: "remove" <>$ capt_arg_payload $+ capt_arg_payload $+ any_arg $--> JavaCollection.remove_at - ; +PatternMatch.Java.implements_collection + ; +map_context_tenv PatternMatch.Java.implements_collection &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back - ; +PatternMatch.Java.implements_queue + ; +map_context_tenv PatternMatch.Java.implements_queue &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back - ; +PatternMatch.Java.implements_lang "StringBuilder" + ; +map_context_tenv( PatternMatch.Java.implements_lang "StringBuilder") &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back - ; +PatternMatch.Java.implements_lang "StringBuilder" + ; +map_context_tenv( PatternMatch.Java.implements_lang "StringBuilder") &:: "setLength" <>$ capt_arg_payload $+...$--> StdVector.invalidate_references ShrinkToFit - ; +PatternMatch.Java.implements_lang "String" + ; +map_context_tenv (PatternMatch.Java.implements_lang "String") &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back - ; +PatternMatch.Java.implements_iterator + ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "remove" <>$ capt_arg_payload $+...$--> JavaIterator.remove ~desc:"remove" - ; +PatternMatch.Java.implements_map &:: "put" <>$ capt_arg_payload - $+...$--> StdVector.push_back - ; +PatternMatch.Java.implements_map &:: "putAll" <>$ capt_arg_payload - $+...$--> StdVector.push_back + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve - ; +PatternMatch.Java.implements_collection + ; +map_context_tenv PatternMatch.Java.implements_collection &:: "get" <>$ capt_arg_payload $+ capt_arg_payload $--> StdVector.at ~desc:"Collection.get()" - ; +PatternMatch.Java.implements_list + ; +map_context_tenv PatternMatch.Java.implements_list &:: "set" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.set - ; +PatternMatch.Java.implements_iterator + ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "hasNext" &--> Misc.nondet ~fn_name:"Iterator.hasNext()" - ; +PatternMatch.Java.implements_enumeration + ; +map_context_tenv PatternMatch.Java.implements_enumeration &:: "hasMoreElements" &--> Misc.nondet ~fn_name:"Enumeration.hasMoreElements()" - ; +PatternMatch.Java.implements_lang "Object" + ; +map_context_tenv( PatternMatch.Java.implements_lang "Object") &:: "equals" &--> Misc.nondet ~fn_name:"Object.equals" - ; +PatternMatch.Java.implements_lang "Iterable" + ; +map_context_tenv (PatternMatch.Java.implements_lang "Iterable") &:: "iterator" <>$ capt_arg_payload $+...$--> JavaIterator.constructor ~desc:"Iterable.iterator" - ; +PatternMatch.Java.implements_iterator + ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "next" <>$ capt_arg_payload $!--> JavaIterator.next ~desc:"Iterator.next()" - ; ( +PatternMatch.Java.implements_enumeration + ; ( +map_context_tenv PatternMatch.Java.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 + ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> C.malloc + ; +map_context_tenv 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 + ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null + ; +map_context_tenv 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 + ; +map_context_tenv 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.__objc_bridge_transfer <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ; +match_builtin BuiltinDecl.__objc_alloc_no_fail <>$ capt_exp $--> ObjC.alloc_not_null - ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg ] ) + ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg + ; +match_regexp_opt Config.pulse_model_skip_pattern + &::.*++> Misc.skip "modelled as skip due to configuration option" ] ) end -let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args +let dispatch tenv proc_name args = ProcNameDispatcher.dispatch (tenv, proc_name) proc_name args diff --git a/infer/tests/codetoanalyze/cpp/pulse/.inferconfig b/infer/tests/codetoanalyze/cpp/pulse/.inferconfig new file mode 100644 index 000000000..26103745a --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/.inferconfig @@ -0,0 +1,3 @@ +{ + "pulse-model-skip-pattern": "skip_model::SkipAll::.*\\|.*SkipSome<.*>::skip_me" +} \ No newline at end of file diff --git a/infer/tests/codetoanalyze/cpp/pulse/skip_config.cpp b/infer/tests/codetoanalyze/cpp/pulse/skip_config.cpp new file mode 100644 index 000000000..096134166 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/skip_config.cpp @@ -0,0 +1,49 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +namespace skip_model { +struct SkipAll { + int* foo() { return nullptr; } + static int* goo() { return nullptr; } +}; + +template +struct SkipSome { + int* skip_me(int**) { return nullptr; } + static int no_skip() { return 42; } +}; + +void test_config_no_skip_ok() { + if (SkipSome>::no_skip() != 42) { + int* p = nullptr; + *p = 42; + } +} + +void test_config_skip_me_ok() { + int* may_be_mutated = nullptr; + int* p = nullptr; + SkipSome> x; + p = x.skip_me(&may_be_mutated); + *p = 42; + *may_be_mutated = 42; +} +} // namespace skip_model + +namespace skip_another_namespace { +void test_config_foo_ok() { + int* p = nullptr; + skip_model::SkipAll x; + p = x.foo(); + *p = 42; +} +void test_config_goo_ok() { + int* p = skip_model::SkipAll::goo(); + *p = 42; +} + +} // namespace skip_another_namespace