[pulse] Add an option for unknown pure model

Summary:
This diff adds an option for unknown pure models, so that their returned values are addressed as the same when the arguments are the same.

In addition, this diff fixes a minor bug on handling pure return values of `return_param`.

Reviewed By: davidpichardie

Differential Revision: D65333946

fbshipit-source-id: 45b687b2c7bb0bda5c5b508c2c1c50f62e8e4e3f

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

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.
 

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).

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

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

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} )

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

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 ->

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
 

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 \

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<std::string> get_value_pure() {
+  if (unknown_pure()) {
+    return std::optional<std::string>{"Godzilla"};
+  }
+  return std::nullopt;
+}
+
+std::string call_get_value_pure_twice_ok() {
+  if (get_value_pure().has_value()) {
+    return *get_value_pure();
+  }
+  return "";
+}