From 03bc3f31c88aed31731b876c3209a6058febdd84 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 17 Sep 2020 04:32:31 -0700 Subject: [PATCH] [pulse] add option to skip functions/classes Summary: This can be useful to make pulse forget about tricky parts of the code. Treat "skipped" procedures as unknown so heuristics for mutating the return value and parameters passed by reference are applied. Reviewed By: ezgicicek Differential Revision: D23729410 fbshipit-source-id: d7a4924a8 --- infer/man/man1/infer-analyze.txt | 3 + infer/man/man1/infer-full.txt | 7 ++ infer/man/man1/infer.txt | 4 + infer/src/absint/ProcnameDispatcher.ml | 2 + infer/src/absint/ProcnameDispatcher.mli | 8 +- infer/src/base/Config.ml | 8 ++ infer/src/base/Config.mli | 2 + infer/src/pulse/PulseModels.ml | 107 ++++++++++++------ .../codetoanalyze/cpp/pulse/.inferconfig | 3 + .../codetoanalyze/cpp/pulse/skip_config.cpp | 49 ++++++++ 10 files changed, 155 insertions(+), 38 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/.inferconfig create mode 100644 infer/tests/codetoanalyze/cpp/pulse/skip_config.cpp 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