[pulse] Add a flag to pass functions that we want to model as returning non-null

Summary: To avoid NULLPTR_DEREFERENCE false positives we want to model some functions as returning non-null. A new flag --pulse-model-return-nonnull allows us to provide a list of such functions.

Reviewed By: ezgicicek

Differential Revision: D22431564

fbshipit-source-id: 9944c7382

infer/man/man1/infer-analyze.txt

@@ -255,6 +255,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-transfer-ownership +string
            Methods that should be modelled as transfering memory ownership in
            Pulse. Accepted formats are method or namespace::method

infer/man/man1/infer-full.txt

@@ -884,6 +884,10 @@ 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-transfer-ownership +string
            Methods that should be modelled as transfering memory ownership in
            Pulse. Accepted formats are method or namespace::method       
@@ -1674,6 +1678,9 @@ INTERNAL OPTIONS
        --pulse-model-release-pattern-reset
            Cancel the effect of --pulse-model-release-pattern.
 
+       --pulse-model-return-nonnull-reset
+           Set --pulse-model-return-nonnull to the empty list.
+
        --pulse-model-transfer-ownership-reset
            Set --pulse-model-transfer-ownership to the empty list.
 

infer/man/man1/infer.txt

@@ -884,6 +884,10 @@ 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-transfer-ownership +string
            Methods that should be modelled as transfering memory ownership in
            Pulse. Accepted formats are method or namespace::method       

infer/src/base/Config.ml

@@ -1842,6 +1842,12 @@ and pulse_model_release_pattern =
     "Regex of methods that should be modelled as release in Pulse"
 
 
+and pulse_model_return_nonnull =
+  CLOpt.mk_string_list ~long:"pulse-model-return-nonnull"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "Methods that should be modelled as returning non-null in Pulse"
+
+
 and pulse_model_transfer_ownership =
   CLOpt.mk_string_list ~long:"pulse-model-transfer-ownership"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -2962,6 +2968,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_nonnull = !pulse_model_return_nonnull
+
 and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
   let models =
     let re = Str.regexp "::" in

infer/src/base/Config.mli

@@ -461,6 +461,8 @@ 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_transfer_ownership_namespace : (string * string) list
 
 val pulse_model_transfer_ownership : string list

infer/src/pulse/PulseModels.ml

@@ -50,6 +50,16 @@ module Misc = struct
     PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue
 
 
+  let return_positive ~desc : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
+    let ret_addr = AbstractValue.mk_fresh () in
+    let ret_value = (ret_addr, [event]) in
+    PulseOperations.write_id ret_id ret_value astate
+    |> PulseArithmetic.and_positive ret_addr
+    |> PulseOperations.ok_continue
+
+
   let return_unknown_size : model =
    fun _ ~callee_procname:_ _location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
@@ -789,7 +799,7 @@ module ProcNameDispatcher = struct
       in
       transfer_ownership_namespace_matchers @ transfer_ownership_name_matchers
     in
-    let abort_matchers =
+    let get_cpp_matchers config ~model =
       let cpp_separator_regex = Str.regexp_string "::" in
       List.filter_map
         ~f:(fun m ->
@@ -797,11 +807,19 @@ module ProcNameDispatcher = struct
           | [] ->
               None
           | first :: rest ->
-              Some (List.fold rest ~f:( &:: ) ~init:(-first) &--> Misc.early_exit) )
-        Config.pulse_model_abort
+              Some (List.fold rest ~f:( &:: ) ~init:(-first) &--> model m) )
+        config
+    in
+    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
     make_dispatcher
-      ( transfer_ownership_matchers @ abort_matchers
+      ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers
       @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
         ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
         ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete

infer/tests/codetoanalyze/cpp/pulse/Makefile

@@ -8,7 +8,7 @@ TESTS_DIR = ../../..
 # see explanations in cpp/biabduction/Makefile for the custom isystem
 CLANG_OPTIONS = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
 INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
---pulse-model-abort "ns1::ns2::fun_abort"
+--pulse-model-abort "ns1::ns2::fun_abort" --pulse-model-return-nonnull "Handle::get"
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.cpp)

infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp

@@ -154,3 +154,29 @@ void set_S() {
 }
 
 int thread_local_was_set_ok() { return T::get()->field; }
+
+struct Item {
+  X* get() const;
+};
+
+struct Handle {
+  X* get() const noexcept {
+    return item_.get() == nullptr ? nullptr : toX(item_);
+  }
+
+  X* operator->() const noexcept {
+    // dynamic check get() != null
+    return get();
+  }
+
+ private:
+  Item item_{};
+  static X* toX(Item item);
+};
+
+// We do not want to report nullptr dereference in this case
+// as we "know" that Item::get does not return null, however
+// at the moment we are not able to show it in pulse.
+// That's why as a workaround we model the analysis of Handle::get`
+// to return non-null
+void explicit_check_for_null_ok(Handle h) { return h->foo(); }