Don't report null dereference on 'this' in C++ methods

Summary: public
`this` can't be null in C++ methods, make backend aware of it.
Behavior for other languages remains the same

Reviewed By: dulmarod

Differential Revision: D2668945

fb-gh-sync-id: c85acbf

infer/src/backend/procAttributes.ml

@@ -26,6 +26,7 @@ type t =
     is_defined : bool; (** true if the procedure is defined, and not just declared *)
     is_generated : bool; (** the procedure has been generated *)
     is_objc_instance_method : bool; (** the procedure is an objective-C instance method *)
+    is_cpp_instance_method : bool; (** the procedure is an C++ instance method *)
     mutable is_synthetic_method : bool; (** the procedure is a synthetic method *)
     language : Config.language; (** language of the procedure *)
     loc : Location.t; (** location of this procedure in the source code *)
@@ -49,6 +50,7 @@ let copy pa =
     is_defined = pa.is_defined;
     is_generated = pa.is_generated;
     is_objc_instance_method = pa.is_objc_instance_method;
+    is_cpp_instance_method = pa.is_cpp_instance_method;
     is_synthetic_method = pa.is_synthetic_method;
     language = pa.language;
     loc = pa.loc;
@@ -71,6 +73,7 @@ let default proc_name language = {
   is_bridge_method = false;
   is_generated = false;
   is_objc_instance_method = false;
+  is_cpp_instance_method = false;
   is_synthetic_method = false;
   language;
   loc = Location.dummy;

infer/src/backend/procAttributes.mli

@@ -24,6 +24,7 @@ type t =
     is_defined : bool; (** true if the procedure is defined, and not just declared *)
     is_generated : bool; (** the procedure has been generated *)
     is_objc_instance_method : bool; (** the procedure is an objective-C instance method *)
+    is_cpp_instance_method : bool; (** the procedure is an C++ instance method *)
     mutable is_synthetic_method : bool; (** the procedure is a synthetic method *)
     language : Config.language; (** language of the procedure *)
     loc : Location.t; (** location of this procedure in the source code *)

infer/src/backend/prover.ml

@@ -815,25 +815,20 @@ let check_inconsistency_base prop =
   let sigma = Prop.get_sigma prop in
   let inconsistent_ptsto _ =
     check_allocatedness prop Sil.exp_zero in
-  let inconsistent_this () = (* "this" cannot be null in Java *)
-    let do_hpred = function
-      | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) ->
-          !Config.curr_language = Config.Java &&
-          Sil.pvar_is_this pv &&
-          Sil.exp_equal e Sil.exp_zero &&
-          Sil.pvar_is_seed pv
-      | _ -> false in
-    IList.exists do_hpred sigma in
-  let inconsistent_self () = (* "self" cannot be null in ObjC *)
+  let inconsistent_this_self_var () =
     let procdesc = Cfg.Node.get_proc_desc (State.get_node ()) in
     let procedure_attr = Cfg.Procdesc.get_attributes procdesc in
+    let is_java_this pvar = !Config.curr_language = Config.Java && Sil.pvar_is_this pvar in
+    let is_objc_instance_self pvar = !Config.curr_language = Config.C_CPP &&
+                                     Sil.pvar_get_name pvar = Mangled.from_string "self" &&
+                                     procedure_attr.ProcAttributes.is_objc_instance_method in
+    let is_cpp_this pvar = !Config.curr_language = Config.C_CPP && Sil.pvar_is_this pvar &&
+                           procedure_attr.ProcAttributes.is_cpp_instance_method in
     let do_hpred = function
       | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) ->
-          !Config.curr_language = Config.C_CPP &&
           Sil.exp_equal e Sil.exp_zero &&
           Sil.pvar_is_seed pv &&
-          Sil.pvar_get_name pv = Mangled.from_string "self" &&
-          procedure_attr.ProcAttributes.is_objc_instance_method
+          (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
       | _ -> false in
     IList.exists do_hpred sigma in
   let inconsistent_atom = function
@@ -859,8 +854,7 @@ let check_inconsistency_base prop =
   || check_inconsistency_two_hpreds prop
   || IList.exists inconsistent_atom pi
   || inconsistent_inequalities ()
-  || inconsistent_this ()
-  || inconsistent_self ()
+  || inconsistent_this_self_var ()
 
 (** Inconsistency checking. *)
 let check_inconsistency prop =

infer/src/clang/cMethod_trans.ml

@@ -289,6 +289,8 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method =
   let pname = Procname.to_string proc_name in
   let attributes = sil_func_attributes_of_attributes (CMethod_signature.ms_get_attributes ms) in
   let is_generated = CMethod_signature.ms_is_generated ms in
+  let is_cpp_inst_method = CMethod_signature.ms_is_instance ms
+                           && CMethod_signature.ms_get_lang ms = CFrontend_config.CPP in
   let create_new_procdesc () =
     let formals = get_formal_parameters tenv ms in
     let captured_str = IList.map (
@@ -311,6 +313,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method =
           is_defined = defined;
           is_generated;
           is_objc_instance_method = is_objc_inst_method;
+          is_cpp_instance_method = is_cpp_inst_method;
           loc = loc_start;
           ret_type;
         } in

infer/tests/codetoanalyze/cpp/errors/npe/this_not_null.cpp

@@ -0,0 +1,17 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+struct X {
+  int f;
+  void init() {}
+  int getF() {
+    init();
+    return f;
+  }
+};

infer/tests/endtoend/cpp/ThisNotNullTest.java

@@ -0,0 +1,63 @@
+/*
+* Copyright (c) 2015 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+package endtoend.cpp;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class ThisNotNullTest {
+
+  public static final String FILE =
+      "infer/tests/codetoanalyze/cpp/errors/npe/this_not_null.cpp";
+
+  private static ImmutableList<String> inferCmd;
+
+  public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder =
+      new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createCPPInferCommand(folder, FILE);
+  }
+
+  @Test
+  public void whenInferRunsOnMethodNoThisNullDerefErrorIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    String[] proceduresWithNullDeref = {
+      /* nothing should be reported */
+    };
+    assertThat(
+        "Results should contain the no null dereference",
+        inferResults,
+        containsExactly(
+            NULL_DEREFERENCE,
+            FILE,
+            proceduresWithNullDeref
+        )
+    );
+  }
+}