diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 75746c2bace..27941a18595 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -825,6 +825,9 @@ PULSE CHECKER OPTIONS Methods that should be modelled as transfering memory ownership in Pulse. Accepted formats are method or namespace::method + --pulse-model-unknown-pure +string + Regex of methods that should be modelled as unknown pure in Pulse + --pulse-models-for-erlang +path Provide custom models for Erlang in JSON files or SQLite3. Files must end with `.json` or `.db` respectively. If a path to a diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index ab1cb195054..615fd454fb2 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1576,6 +1576,10 @@ OPTIONS Pulse. Accepted formats are method or namespace::method See also infer-analyze(1). + --pulse-model-unknown-pure +string + Regex of methods that should be modelled as unknown pure in Pulse + See also infer-analyze(1). + --pulse-model-unreachable +string Methods to be modeled as unreachable. See also infer-analyze(1). @@ -3119,6 +3123,9 @@ INTERNAL OPTIONS --pulse-model-transfer-ownership-reset Set --pulse-model-transfer-ownership to the empty list. + --pulse-model-unknown-pure-reset + Set --pulse-model-unknown-pure to the empty list. + --pulse-model-unreachable-reset Set --pulse-model-unreachable to the empty list. diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 65bc58a1106..3e4a18ff74e 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1576,6 +1576,10 @@ OPTIONS Pulse. Accepted formats are method or namespace::method See also infer-analyze(1). + --pulse-model-unknown-pure +string + Regex of methods that should be modelled as unknown pure in Pulse + See also infer-analyze(1). + --pulse-model-unreachable +string Methods to be modeled as unreachable. See also infer-analyze(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 4aa61e87dc0..acc5bcdedcc 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2597,6 +2597,12 @@ and pulse_model_skip_pattern_list = "Regex of methods that should be modelled as \"skip\" in Pulse" +and pulse_model_unknown_pure = + CLOpt.mk_string_list ~long:"pulse-model-unknown-pure" + ~in_help:InferCommand.[(Analyze, manual_pulse)] + "Regex of methods that should be modelled as unknown pure in Pulse" + + and pulse_model_unreachable = CLOpt.mk_string_list ~long:"pulse-model-unreachable" ~in_help:InferCommand.[(Analyze, manual_clang)] @@ -4537,6 +4543,8 @@ and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership = RevList.rev_partition_map ~f:aux models +and pulse_model_unknown_pure = join_patterns_list (RevList.to_list !pulse_model_unknown_pure) + and pulse_model_unreachable = RevList.to_list !pulse_model_unreachable and pulse_models_for_erlang = RevList.to_list !pulse_models_for_erlang diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 176073bed5f..28a8f0f4f4d 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -672,6 +672,8 @@ val pulse_model_transfer_ownership : string list val pulse_model_transfer_ownership_namespace : (string * string) list +val pulse_model_unknown_pure : Str.regexp option + val pulse_model_unreachable : string list val pulse_models_for_erlang : string list diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 4f16047ba57..38af931689e 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -81,7 +81,7 @@ module GlobalForStats = struct end let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallEvent.t) - callee_pname_opt ~ret ~actuals ~formals_opt astate0 = + ?(force_pure = false) callee_pname_opt ~ret ~actuals ~formals_opt astate0 = let hist = let actuals_hists = List.map actuals ~f:(fun ((_, hist), _) -> hist) in ValueHistory.unknown_call reason actuals_hists call_loc timestamp @@ -91,9 +91,9 @@ let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallE let astate = add_returned_from_unknown callee_pname_opt ret_val actuals astate0 in let astate = PulseOperations.write_id (fst ret) (ret_val, hist) astate in let astate = Decompiler.add_call_source ret_val reason actuals astate in - (* set to [false] if we think the procedure called does not behave "functionally", i.e. return the - same value for the same inputs *) - let is_functional = ref true in + (* set to [false] if we think the procedure called does not behave "purely", i.e. return the same + value for the same inputs *) + let is_pure = ref true in let should_havoc actual_typ formal_typ_opt = match actual_typ.Typ.desc with | _ when not Config.pulse_havoc_arguments -> @@ -122,7 +122,7 @@ let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallE (* We should not havoc when the corresponding formal is a pointer to const *) match should_havoc actual_typ (Option.map ~f:snd formal_opt) with | `ShouldHavoc -> - is_functional := false ; + is_pure := false ; (* this will deallocate anything reachable from the [actual] and havoc the values pointed to by [actual] *) let astate = @@ -193,7 +193,15 @@ let unknown_call tenv ({PathContext.timestamp} as path) call_loc (reason : CallE in let++ astate = match f with - | Some f when !is_functional -> + | Some f when !is_pure || force_pure -> + let ret_val = + match (Option.bind formals_opt ~f:List.last, List.last actuals) with + | Some (pvar, _), Some ((return_param_val, _), _) + when Mangled.is_return_param (Pvar.get_name pvar) -> + return_param_val + | _ -> + ret_val + in PulseArithmetic.and_equal (AbstractValueOperand ret_val) (FunctionApplicationOperand {f; actuals= List.map ~f:(fun ((actual_val, _hist), _typ) -> actual_val) actuals} ) diff --git a/infer/src/pulse/PulseCallOperations.mli b/infer/src/pulse/PulseCallOperations.mli index 8bf7484db9f..fa2c7240de7 100644 --- a/infer/src/pulse/PulseCallOperations.mli +++ b/infer/src/pulse/PulseCallOperations.mli @@ -35,6 +35,7 @@ val unknown_call : -> PathContext.t -> Location.t -> CallEvent.t + -> ?force_pure:bool -> Procname.t option -> ret:Ident.t * Typ.t -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list diff --git a/infer/src/pulse/PulseModelsImport.ml b/infer/src/pulse/PulseModelsImport.ml index 3ff27e81fea..43bba5f5bd5 100644 --- a/infer/src/pulse/PulseModelsImport.ml +++ b/infer/src/pulse/PulseModelsImport.ml @@ -190,7 +190,7 @@ module Basic = struct (** 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_no_non_disj = + let unknown_call ?(force_pure = false) skip_reason args : model_no_non_disj = fun {path; callee_procname; analysis_data= {tenv}; location; ret} astate -> let actuals = List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} -> @@ -199,8 +199,11 @@ module Basic = struct let formals_opt = IRAttributes.load callee_procname |> Option.map ~f:ProcAttributes.get_pvar_formals in + let reason = + if force_pure then CallEvent.SkippedKnownCall callee_procname else CallEvent.Model skip_reason + in let<++> astate = - PulseCallOperations.unknown_call tenv path location (Model skip_reason) (Some callee_procname) + PulseCallOperations.unknown_call tenv path location reason ~force_pure (Some callee_procname) ~ret ~actuals ~formals_opt astate in astate @@ -454,6 +457,8 @@ module Basic = struct ~desc:"modelled as returning the first argument due to configuration option" ; +match_regexp_opt Config.pulse_model_skip_pattern &::.*++> unknown_call "modelled as skip due to configuration option" + ; +match_regexp_opt Config.pulse_model_unknown_pure + &::.*++> unknown_call ~force_pure:true "modelled unknown pure due to configuration option" ; +match_taint_source Config.pulse_taint_skip_sources &::.*++> unknown_call "modelled as skip due to configuration option" ] |> List.map ~f:(fun matcher -> diff --git a/infer/src/pulse/PulseModelsImport.mli b/infer/src/pulse/PulseModelsImport.mli index 59e78b14ed4..5146d604f86 100644 --- a/infer/src/pulse/PulseModelsImport.mli +++ b/infer/src/pulse/PulseModelsImport.mli @@ -177,7 +177,8 @@ module Basic : sig (AbstractValue.t * ValueHistory.t) ProcnameDispatcher.Call.FuncArg.t -> model_no_non_disj val unknown_call : - string + ?force_pure:bool + -> string -> (AbstractValue.t * ValueHistory.t) ProcnameDispatcher.Call.FuncArg.t list -> model_no_non_disj diff --git a/infer/tests/codetoanalyze/cpp/pulse-17/Makefile b/infer/tests/codetoanalyze/cpp/pulse-17/Makefile index 35c87b79a46..3b1e4136bf3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse-17/Makefile +++ b/infer/tests/codetoanalyze/cpp/pulse-17/Makefile @@ -9,6 +9,7 @@ TESTS_DIR = ../../.. CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c INFER_OPTIONS = \ --pulse-only --debug-exceptions --no-pulse-force-continue --project-root $(TESTS_DIR) \ + --pulse-model-unknown-pure get_value_pure \ --pulse-report-issues-for-tests INFERPRINT_OPTIONS = \ --issues-tests-fields file,procedure,line_offset,bug_type,bucket,severity,bug_trace,taint_extra,transitive_callees_extra,autofix \ diff --git a/infer/tests/codetoanalyze/cpp/pulse-17/std_optional.cpp b/infer/tests/codetoanalyze/cpp/pulse-17/std_optional.cpp index 929e3dda3b6..f3bd0825248 100644 --- a/infer/tests/codetoanalyze/cpp/pulse-17/std_optional.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse-17/std_optional.cpp @@ -163,3 +163,19 @@ std::string inside_try_catch_FP(const std::string& x) { return ""; } } + +int unknown_pure(); + +std::optional get_value_pure() { + if (unknown_pure()) { + return std::optional{"Godzilla"}; + } + return std::nullopt; +} + +std::string call_get_value_pure_twice_ok() { + if (get_value_pure().has_value()) { + return *get_value_pure(); + } + return ""; +}