From 95a12d9706a78fff791e9800711d8432868e7f31 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A1zaro=20Clapp=20Jim=C3=A9nez=20Labora?=
 <lazaroclapp@fb.com>
Date: Thu, 23 Jun 2016 16:35:21 -0700
Subject: [PATCH] model String.equals(...) as '=='

Reviewed By: sblackshear

Differential Revision: D3468427

fbshipit-source-id: 852ef5f
---
 infer/models/java/src/java/lang/String.java   |  8 ++++
 .../expected_outputs/ant_report.json          | 10 +++++
 .../expected_outputs/buck_report.json         | 10 +++++
 .../java/infer/NullPointerExceptions.java     | 40 +++++++++++++++++++
 .../java/infer/NullPointerExceptionTest.java  |  2 +
 5 files changed, 70 insertions(+)

diff --git a/infer/models/java/src/java/lang/String.java b/infer/models/java/src/java/lang/String.java
index 6cc4e25e6..ec1eb3751 100644
--- a/infer/models/java/src/java/lang/String.java
+++ b/infer/models/java/src/java/lang/String.java
@@ -54,4 +54,12 @@ public final class String {
             throw new StringIndexOutOfBoundsException(offset + length);
     }
 
+    public boolean equals(Object anObject) {
+        if (this == anObject) {
+          return true;
+        } else {
+          return InferUndefined.boolean_undefined();
+        }
+    }
+
 }
diff --git a/infer/tests/build_systems/expected_outputs/ant_report.json b/infer/tests/build_systems/expected_outputs/ant_report.json
index f68869805..65c65ef12 100644
--- a/infer/tests/build_systems/expected_outputs/ant_report.json
+++ b/infer/tests/build_systems/expected_outputs/ant_report.json
@@ -784,6 +784,16 @@
     "file": "codetoanalyze/java/infer/CloseableAsResourceExample.java",
     "procedure": "T CloseableAsResourceExample.sourceOfNullWithResourceLeak()"
   },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP()"
+  },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.stringVarEqualsFalseNPE()"
+  },
   {
     "bug_type": "NULL_DEREFERENCE",
     "file": "codetoanalyze/java/infer/NullPointerExceptions.java",
diff --git a/infer/tests/build_systems/expected_outputs/buck_report.json b/infer/tests/build_systems/expected_outputs/buck_report.json
index a0374eb9a..ae8bc50c4 100644
--- a/infer/tests/build_systems/expected_outputs/buck_report.json
+++ b/infer/tests/build_systems/expected_outputs/buck_report.json
@@ -784,6 +784,16 @@
     "file": "infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java",
     "procedure": "T CloseableAsResourceExample.sourceOfNullWithResourceLeak()"
   },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP()"
+  },
+  {
+    "bug_type": "NULL_DEREFERENCE",
+    "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
+    "procedure": "void NullPointerExceptions.stringVarEqualsFalseNPE()"
+  },
   {
     "bug_type": "NULL_DEREFERENCE",
     "file": "infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java",
diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
index 21a2bb147..dc4acce30 100644
--- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
+++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
@@ -563,5 +563,45 @@ public class NullPointerExceptions {
     o.orNull().toString();
   }
 
+  void stringConstantEqualsTrueNotNPE() {
+    final String c1 = "Test string!";
+    final String c2 = "Test string!";
+    String s = null;
+    if(c1.equals(c1)) {
+      s = "safe";
+    }
+    s.toString(); // No NPE
+    s = null;
+    if(c1.equals(c2)) {
+      s = "safe";
+    }
+    s.toString(); // No NPE
+  }
+
+  void stringConstantEqualsFalseNotNPE_FP() {
+    // This won't actually cause an NPE, but our current model for String.equals
+    // returns boolean_undefined for all cases other than String constant
+    // equality. Consider handling constant inequality in the future.
+    final String c1 = "Test string 1";
+    final String c2 = "Test string 2";
+    String s = null;
+    if(!c1.equals(c2)) {
+      s = "safe";
+    }
+    s.toString(); // No NPE
+  }
+
+  String getString2() {
+    return "string 2";
+  }
+
+  void stringVarEqualsFalseNPE() {
+    final String c1 = "Test string 1";
+    String c2 = "Test " + getString2();
+    String s = null;
+    if(!c1.equals(c2)) {
+      s.toString(); // NPE
+    }
+  }
 
 }
diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java
index aea1cabf2..99e728dc5 100644
--- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java
+++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java
@@ -75,6 +75,8 @@ public class NullPointerExceptionTest {
         "dereferenceAfterUnlock1",
         "dereferenceAfterUnlock2",
         "optionalNPE",
+        "stringVarEqualsFalseNPE",
+        "stringConstantEqualsFalseNotNPE_FP",
     };
     assertThat(
         "Results should contain " + NULL_DEREFERENCE,