[pulse] Add a flag to pass functions that we want to model as abort

Summary: To avoid NULLPTR_DEREFERENCE false positives we want to treat some functions as `abort`. A new flag `--pulse-model-abort` allows us to provide a list of such functions.

Reviewed By: ezgicicek

Differential Revision: D21962555

fbshipit-source-id: d46b93c99

infer/man/man1/infer-analyze.txt

@@ -236,6 +236,9 @@ OPTIONS
            be used on pathologically large procedures to prevent too-big
            states from being produced.
 
+       --pulse-model-abort +string
+           Methods that should be modelled as abort in Pulse
+
        --pulse-model-alloc-pattern string
            Regex of methods that should be modelled as allocs in Pulse
 

infer/man/man1/infer-full.txt

@@ -901,6 +901,9 @@ OPTIONS
            be used on pathologically large procedures to prevent too-big
            states from being produced.           See also infer-analyze(1).
 
+       --pulse-model-abort +string
+           Methods that should be modelled as abort in Pulse           See also infer-analyze(1).
+
        --pulse-model-alloc-pattern string
            Regex of methods that should be modelled as allocs in Pulse       
     See also infer-analyze(1).
@@ -1687,6 +1690,9 @@ INTERNAL OPTIONS
        --pulse-max-disjuncts int
            Under-approximate after int disjunctions in the domain
 
+       --pulse-model-abort-reset
+           Set --pulse-model-abort to the empty list.
+
        --pulse-model-alloc-pattern-reset
            Cancel the effect of --pulse-model-alloc-pattern.
 

infer/man/man1/infer.txt

@@ -901,6 +901,9 @@ OPTIONS
            be used on pathologically large procedures to prevent too-big
            states from being produced.           See also infer-analyze(1).
 
+       --pulse-model-abort +string
+           Methods that should be modelled as abort in Pulse           See also infer-analyze(1).
+
        --pulse-model-alloc-pattern string
            Regex of methods that should be modelled as allocs in Pulse       
     See also infer-analyze(1).

infer/src/base/Config.ml

@@ -1841,6 +1841,12 @@ and pulse_max_disjuncts =
     "Under-approximate after $(i,int) disjunctions in the domain"
 
 
+and pulse_model_abort =
+  CLOpt.mk_string_list ~long:"pulse-model-abort"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "Methods that should be modelled as abort in Pulse"
+
+
 and pulse_model_alloc_pattern =
   CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -2981,6 +2987,8 @@ and pulse_intraprocedural_only = !pulse_intraprocedural_only
 
 and pulse_max_disjuncts = !pulse_max_disjuncts
 
+and pulse_model_abort = !pulse_model_abort
+
 and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_pattern
 
 and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern

infer/src/base/Config.mli

@@ -461,6 +461,8 @@ val pulse_intraprocedural_only : bool
 
 val pulse_max_disjuncts : int
 
+val pulse_model_abort : string list
+
 val pulse_model_alloc_pattern : Str.regexp option
 
 val pulse_model_release_pattern : Str.regexp option

infer/src/pulse/PulseModels.ml

@@ -713,8 +713,19 @@ module ProcNameDispatcher = struct
       in
       transfer_ownership_namespace_matchers @ transfer_ownership_name_matchers
     in
+    let abort_matchers =
+      let cpp_separator_regex = Str.regexp_string "::" in
+      List.filter_map
+        ~f:(fun m ->
+          match Str.split cpp_separator_regex m with
+          | [] ->
+              None
+          | first :: rest ->
+              Some (List.fold rest ~f:( &:: ) ~init:(-first) &--> Misc.early_exit) )
+        Config.pulse_model_abort
+    in
     make_dispatcher
-      ( transfer_ownership_matchers
+      ( transfer_ownership_matchers @ abort_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

@@ -7,7 +7,8 @@ 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)
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
+--pulse-model-abort "ns1::ns2::fun_abort"
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.cpp)

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

@@ -6,6 +6,8 @@
  */
 
 #include <type_traits>
+#include <atomic>
+#include <cstdlib>
 
 void assign_zero_ok() {
   int x[2];
@@ -90,3 +92,33 @@ void std_false_type_deref_bad() {
     *x = 42;
   }
 }
+
+std::atomic<bool> global_var{true};
+
+namespace ns1 {
+namespace ns2 {
+void fun_abort(bool b) {
+  bool abort = true;
+  if (b) {
+    abort = global_var.load();
+  } else {
+    abort = true;
+  }
+  if (abort) {
+    std::abort();
+  }
+}
+} // namespace ns2
+} // namespace ns1
+
+X* getX(bool b) {
+  if (b) {
+    return new X();
+  } else {
+    ns1::ns2::fun_abort(true);
+  }
+
+  return nullptr;
+}
+
+void call_modeled_abort_ok() { getX(false)->foo(); }