[infer][backend] Extend the scope of NULL_TEST_AFTER_DEREFERENCE check

Reviewed By: sblackshear

Differential Revision: D5580382

fbshipit-source-id: 425ff7f

infer/src/backend/symExec.ml

@@ -464,6 +464,17 @@ let check_already_dereferenced tenv pname cond prop =
     | Exp.BinOp ((Binop.Eq | Binop.Ne), Exp.Var id, Exp.Const Const.Cint i)
       when IntLit.iszero i
      -> Some id
+    (* These two patterns appear frequently in Prune nodes *)
+    | Exp.BinOp
+        ( (Binop.Eq | Binop.Ne)
+        , Exp.BinOp (Binop.Eq, Exp.Var id, Exp.Const Const.Cint i)
+        , Exp.Const Const.Cint j )
+    | Exp.BinOp
+        ( (Binop.Eq | Binop.Ne)
+        , Exp.BinOp (Binop.Eq, Exp.Const Const.Cint i, Exp.Var id)
+        , Exp.Const Const.Cint j )
+      when IntLit.iszero i && IntLit.iszero j
+     -> Some id
     | _
      -> None
   in

infer/tests/codetoanalyze/c/errors/issues.exp

@@ -89,6 +89,7 @@ codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, l_error, 2, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, m, 2, NULL_TEST_AFTER_DEREFERENCE
+codetoanalyze/c/errors/null_test_after_deref/basic.c, null_test_deref_basic_bad, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/resource_leaks/leak.c, fileNotClosed, 5, RESOURCE_LEAK
 codetoanalyze/c/errors/resource_leaks/leak.c, socketNotClosed, 5, RESOURCE_LEAK
 codetoanalyze/c/errors/sizeof/sizeof_706.c, sentinel_bad, 0, DIVIDE_BY_ZERO

infer/tests/codetoanalyze/c/errors/null_test_after_deref/basic.c

@@ -0,0 +1,23 @@
+/*
+ * Copyright (c) 2017 - 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.
+ */
+int null_test_deref_basic_bad(int* p) {
+  int ret = *p;
+  if (p == 0)
+    return -1;
+  return ret;
+}
+
+int null_test_deref_basic_ok() {
+  int x = 0;
+  int* p = &x;
+  int ret = *p;
+  if (p == 0)
+    return -1;
+  return ret;
+}