From 713cdbf580fdd819386163b6e80469d35a666273 Mon Sep 17 00:00:00 2001
From: Daiva Naudziuniene <daivan@fb.com>
Date: Wed, 5 May 2021 03:12:17 -0700
Subject: [PATCH] [pulse] Inline initializers for global constant accesses

Summary: Not tracking values for global constants might cause nullptr_dereference false positives. In particular, if the code has multiple checks and uses a global constant by its name in one check and its value in another check (see added test case), we are not able prune infeasible paths. This diff addresses such false positives by inlining initializers of global constants when they are being used.  An assumption is that most the time the initialization of global constants would not have side effects.

Reviewed By: jvillard

Differential Revision: D25994898

fbshipit-source-id: 26360c4de
---
 infer/src/pulse/Pulse.ml                      | 50 +++++++++++++++----
 .../tests/codetoanalyze/cpp/pulse/nullptr.cpp | 35 +++++++++++++
 2 files changed, 75 insertions(+), 10 deletions(-)

diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 9881ebc86..50c80a2d4 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -283,17 +283,47 @@ module PulseTransferFunctions = struct
       match instr with
       | Load {id= lhs_id; e= rhs_exp; loc} ->
           (* [lhs_id := *rhs_exp] *)
-          let result =
-            if Config.pulse_isl then
-              PulseOperations.eval_deref_isl loc rhs_exp astate
-              |> List.map ~f:(fun result ->
-                     let+ astate, rhs_addr_hist = result in
-                     PulseOperations.write_id lhs_id rhs_addr_hist astate )
-            else
-              [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
-                 PulseOperations.write_id lhs_id rhs_addr_hist astate) ]
+          let deref_rhs astate =
+            let result =
+              if Config.pulse_isl then
+                PulseOperations.eval_deref_isl loc rhs_exp astate
+                |> List.map ~f:(fun result ->
+                       let+ astate, rhs_addr_hist = result in
+                       PulseOperations.write_id lhs_id rhs_addr_hist astate )
+              else
+                [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
+                   PulseOperations.write_id lhs_id rhs_addr_hist astate) ]
+            in
+            PulseReport.report_results tenv proc_desc err_log result
           in
-          PulseReport.report_results tenv proc_desc err_log result
+          let set_global_astates =
+            match rhs_exp with
+            | Lvar pvar when Pvar.is_global pvar && Pvar.is_compile_constant pvar -> (
+              (* Inline initializers of global constants when they are being used.
+                 This addresses nullptr false positives by pruning infeasable paths global_var != global_constant_value,
+                 where global_constant_value is the value of global_var *)
+              (* TODO: Initial global constants only once *)
+              match Pvar.get_initializer_pname pvar with
+              | Some proc_name ->
+                  let call_flags = CallFlags.default in
+                  let ret_id_void = (Ident.create_fresh Ident.knormal, StdTyp.void) in
+                  let no_error_states =
+                    dispatch_call analysis_data ret_id_void (Const (Cfun proc_name)) [] loc
+                      call_flags astate
+                    |> List.filter_map ~f:(function
+                         | Ok (ContinueProgram astate) ->
+                             Some astate
+                         | _ ->
+                             (* ignore errors in global initializers *)
+                             None )
+                  in
+                  if List.is_empty no_error_states then [astate] else no_error_states
+              | None ->
+                  [astate] )
+            | _ ->
+                [astate]
+          in
+          List.concat_map set_global_astates ~f:deref_rhs
       | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
           (* [*lhs_exp := rhs_exp] *)
           let event = ValueHistory.Assignment loc in
diff --git a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp
index ed4d067c7..fd1045501 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp
@@ -8,6 +8,7 @@
 #include <type_traits>
 #include <atomic>
 #include <cstdlib>
+#include <string>
 
 void assign_zero_ok() {
   int x[2];
@@ -215,3 +216,37 @@ void test_after_dereference2_latent(int* x) {
 void call_test_after_dereference2_bad() {
   test_after_dereference2_latent(NULL);
 }
+
+enum Type { STRING };
+
+static constexpr Type typeGlobal = STRING;
+
+struct D {
+  Type type;
+  std::string string;
+
+  D(std::string s) : type(STRING) { new (&string) std::string(std::move(s)); }
+
+  std::string const* get() const& {
+    if (type != typeGlobal) {
+      return nullptr;
+    }
+    return &string;
+  }
+
+  std::string to(const std::string& value) const { return value.c_str(); };
+
+  std::string asString() const {
+    if (type == STRING) {
+      const std::string& value = *get();
+      return to(value);
+    }
+    return "";
+  }
+};
+
+std::string global_const_skipped_function_ok() {
+  D* s = new D("");
+  std::shared_ptr<D> ptr(s);
+  return ptr->asString();
+}