From 583a011666f635b9c50e91449599006529b9e749 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 19 Mar 2021 09:50:33 -0700 Subject: [PATCH] [pulse] Add a new config for modelling a function as returning the first arg Summary: Adding a new config for pulse `--pulse-model-return-first-arg` Reviewed By: skcho Differential Revision: D27186448 fbshipit-source-id: 938b65267 --- infer/man/man1/infer-analyze.txt | 4 ++++ infer/man/man1/infer-full.txt | 7 +++++++ infer/man/man1/infer.txt | 4 ++++ infer/src/base/Config.ml | 8 ++++++++ infer/src/base/Config.mli | 2 ++ infer/src/pulse/PulseModels.ml | 21 +++++++++++++++------ 6 files changed, 40 insertions(+), 6 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index ca8322bb3..e00e0c0ea 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -280,6 +280,10 @@ OPTIONS --pulse-model-release-pattern string Regex of methods that should be modelled as release in Pulse + --pulse-model-return-first-arg string + Regex of methods that should be modelled as returning the first + argument in Pulse + --pulse-model-return-nonnull string Regex of methods that should be modelled as returning non-null in Pulse diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index c5b33eeb7..e867956a0 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -992,6 +992,10 @@ OPTIONS Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). + --pulse-model-return-first-arg string + Regex of methods that should be modelled as returning the first + argument 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). @@ -1885,6 +1889,9 @@ INTERNAL OPTIONS --pulse-model-release-pattern-reset Cancel the effect of --pulse-model-release-pattern. + --pulse-model-return-first-arg-reset + Cancel the effect of --pulse-model-return-first-arg. + --pulse-model-return-nonnull-reset Cancel the effect of --pulse-model-return-nonnull. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 140c62c4f..87ca28133 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -992,6 +992,10 @@ OPTIONS Regex of methods that should be modelled as release in Pulse See also infer-analyze(1). + --pulse-model-return-first-arg string + Regex of methods that should be modelled as returning the first + argument 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). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 16a27c318..86a009375 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1949,6 +1949,12 @@ and pulse_model_return_nonnull = "Regex of methods that should be modelled as returning non-null in Pulse" +and pulse_model_return_first_arg = + CLOpt.mk_string_opt ~long:"pulse-model-return-first-arg" + ~in_help:InferCommand.[(Analyze, manual_generic)] + "Regex of methods that should be modelled as returning the first argument in Pulse" + + and pulse_model_skip_pattern = CLOpt.mk_string_opt ~long:"pulse-model-skip-pattern" ~in_help:InferCommand.[(Analyze, manual_generic)] @@ -3208,6 +3214,8 @@ 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_first_arg = Option.map ~f:Str.regexp !pulse_model_return_first_arg + 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 54761209f..b860d7381 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -493,6 +493,8 @@ val pulse_model_alloc_pattern : Str.regexp option val pulse_model_release_pattern : Str.regexp option +val pulse_model_return_first_arg : Str.regexp option + 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 99e2e1f1a..e8c49fe19 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -114,9 +114,11 @@ module Misc = struct PulseOperations.havoc_id ret_id [event] astate |> ok_continue - let id_first_arg arg_access_hist : model = - fun _ ~callee_procname:_ _ ~ret astate -> - PulseOperations.write_id (fst ret) arg_access_hist astate |> ok_continue + let id_first_arg ~desc (arg_value, arg_history) : model = + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let ret_value = (arg_value, event :: arg_history) in + PulseOperations.write_id ret_id ret_value astate |> ok_continue let free_or_delete operation deleted_access : model = @@ -1159,11 +1161,13 @@ module ProcNameDispatcher = struct $--> Misc.alloc_not_null_call_ev ~desc:"new" ; +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.__cast + <>$ capt_arg_payload $+...$--> Misc.id_first_arg ~desc:"cast" ; +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 + <>$ capt_arg_payload + $+...$--> Misc.id_first_arg ~desc:"infer_init_list" ; +map_context_tenv (PatternMatch.Java.implements_lang "System") &:: "exit" <>--> Misc.early_exit ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size @@ -1460,10 +1464,15 @@ module ProcNameDispatcher = struct ; +match_builtin BuiltinDecl.__objc_alloc_no_fail <>$ capt_exp $--> ObjC.alloc_not_null_alloc_ev ~desc:"alloc" - ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg + ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg ~desc:"NSObject.init" ; +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_return_first_arg + &::+ (fun _ _ -> true) + <>$ capt_arg_payload + $+...$--> Misc.id_first_arg + ~desc:"modelled as returning the first argument due to configuration option" ; +match_regexp_opt Config.pulse_model_skip_pattern &::.*++> Misc.skip "modelled as skip due to configuration option" ] ) end