From bc49f1deb16fef22e0a4581d5f49f57cdd677531 Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Fri, 12 Feb 2021 07:16:19 -0800 Subject: [PATCH] [pulse] Adapting --pulse-model-return-nonnull for Java Summary: The `--pulse-model-return-nonnull` config option currently works for C++. Now we will be using it also for Java. Changing type from string list to regexp to make it more general. Reviewed By: ezgicicek Differential Revision: D26367888 fbshipit-source-id: 9a06b9b32 --- infer/man/man1/infer-analyze.txt | 5 +++-- infer/man/man1/infer-full.txt | 8 ++++---- infer/man/man1/infer.txt | 6 +++--- infer/src/base/Config.ml | 6 +++--- infer/src/base/Config.mli | 2 +- infer/src/pulse/PulseModels.ml | 10 ++++------ infer/tests/codetoanalyze/cpp/pulse/.inferconfig | 2 +- 7 files changed, 19 insertions(+), 20 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 704303c9d..f37c64289 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -271,8 +271,9 @@ OPTIONS --pulse-model-release-pattern string Regex of methods that should be modelled as release in Pulse - --pulse-model-return-nonnull +string - Methods that should be modelled as returning non-null in Pulse + --pulse-model-return-nonnull string + Regex of 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 diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 45400f0af..6ffe40b46 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -955,9 +955,9 @@ OPTIONS Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). - --pulse-model-return-nonnull +string - Methods that should be modelled as returning non-null in Pulse - See also infer-analyze(1). + --pulse-model-return-nonnull string + Regex of 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 @@ -1820,7 +1820,7 @@ INTERNAL OPTIONS Cancel the effect of --pulse-model-release-pattern. --pulse-model-return-nonnull-reset - Set --pulse-model-return-nonnull to the empty list. + Cancel the effect of --pulse-model-return-nonnull. --pulse-model-skip-pattern-reset Cancel the effect of --pulse-model-skip-pattern. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 8b2b66c0e..b5d45721a 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -955,9 +955,9 @@ OPTIONS Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). - --pulse-model-return-nonnull +string - Methods that should be modelled as returning non-null in Pulse - See also infer-analyze(1). + --pulse-model-return-nonnull string + Regex of 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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index b417b0102..f029ec892 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1905,9 +1905,9 @@ and pulse_model_release_pattern = and pulse_model_return_nonnull = - CLOpt.mk_string_list ~long:"pulse-model-return-nonnull" + CLOpt.mk_string_opt ~long:"pulse-model-return-nonnull" ~in_help:InferCommand.[(Analyze, manual_generic)] - "Methods that should be modelled as returning non-null in Pulse" + "Regex of methods that should be modelled as returning non-null in Pulse" and pulse_model_skip_pattern = @@ -3137,7 +3137,7 @@ 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_return_nonnull = RevList.to_list !pulse_model_return_nonnull +and pulse_model_return_nonnull = Option.map ~f:Str.regexp !pulse_model_return_nonnull and pulse_model_skip_pattern = Option.map ~f:Str.regexp !pulse_model_skip_pattern diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0d2cf09bb..17d4ae328 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -481,7 +481,7 @@ val pulse_model_alloc_pattern : Str.regexp option val pulse_model_release_pattern : Str.regexp option -val pulse_model_return_nonnull : string list +val pulse_model_return_nonnull : Str.regexp option val pulse_model_skip_pattern : Str.regexp option diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index e05eefab4..e687ca7ef 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1075,11 +1075,6 @@ module ProcNameDispatcher = struct let abort_matchers = get_cpp_matchers ~model:(fun _ -> Misc.early_exit) Config.pulse_model_abort in - let return_nonnull_matchers = - get_cpp_matchers - ~model:(fun m -> Misc.return_positive ~desc:m) - Config.pulse_model_return_nonnull - in let match_regexp_opt r_opt (_tenv, proc_name) _ = Option.exists r_opt ~f:(fun r -> let s = Procname.to_string proc_name in @@ -1087,7 +1082,7 @@ module ProcNameDispatcher = struct in let map_context_tenv f (x, _) = f x in make_dispatcher - ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers + ( transfer_ownership_matchers @ abort_matchers @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free ; +match_builtin BuiltinDecl.malloc <>$ capt_exp $--> C.malloc ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete @@ -1382,6 +1377,9 @@ module ProcNameDispatcher = struct <>$ 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 + ; +match_regexp_opt Config.pulse_model_return_nonnull + &::.*--> Misc.return_positive + ~desc:"modelled as returning not null due to configuration option" ; +match_regexp_opt Config.pulse_model_skip_pattern &::.*++> Misc.skip "modelled as skip due to configuration option" ] ) end diff --git a/infer/tests/codetoanalyze/cpp/pulse/.inferconfig b/infer/tests/codetoanalyze/cpp/pulse/.inferconfig index 8484ba08d..f67f0e15a 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/.inferconfig +++ b/infer/tests/codetoanalyze/cpp/pulse/.inferconfig @@ -1,5 +1,5 @@ { "pulse-model-abort": ["ns1::ns2::fun_abort"], - "pulse-model-return-nonnull": ["Handle::get"], + "pulse-model-return-nonnull": "Handle::get", "pulse-model-skip-pattern": "skip_model::SkipAll::.*\\|.*SkipSome<.*>::skip_me" }