model String.equals(...) as '=='

Reviewed By: sblackshear

Differential Revision: D3468427

fbshipit-source-id: 852ef5f

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();
+        }
+    }
+
 }

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",

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",

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
+    }
+  }
 
 }

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,