[infer][java] modeling more methods for HashMap

Summary: Model the `remove(...)` and the `clear()` method of `HashMap`.

Reviewed By: sblackshear

Differential Revision: D5887674

fbshipit-source-id: c3f40ee

infer/models/java/src/java/util/HashMap.java

@@ -11,6 +11,7 @@ package java.util;
 import java.io.*;
 
 import com.facebook.infer.builtins.InferUndefined;
+import com.facebook.infer.builtins.InferBuiltins;
 
 /**
  * A recency abstraction for hashmaps that remembers only the last two
@@ -60,6 +61,16 @@ public abstract class HashMap<K,V> {
     return null;
   }
 
+  public V remove(K key) {
+    V value = get(key);
+    removeKey(key);
+    return value;
+  }
+
+  public void clear() {
+    lastKey1 = null;
+    lastKey2 = null;
+  }
 
   /** some sort of circular buffer simulator */
   private void pushKey(K key) {
@@ -71,6 +82,15 @@ public abstract class HashMap<K,V> {
       return areEqual(key, lastKey1) || areEqual(key, lastKey2);
   }
 
+  private void removeKey(K key) {
+    if (areEqual(key, lastKey1)) {
+      lastKey1 = null;
+    }
+    if (areEqual(key, lastKey2)) {
+      lastKey2 = null;
+    }
+  }
+
   private boolean areEqual(K x, K y) {
     return x == y;
   }

infer/tests/build_systems/ant/issues.exp

@@ -76,6 +76,8 @@ codetoanalyze/java/infer/GuardedByExample.java, void GuardedByExample.writeFAfte
 codetoanalyze/java/infer/GuardedByExample.java, void GuardedByExample.writeFBad(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure writeFBad()]
 codetoanalyze/java/infer/GuardedByExample.java, void GuardedByExample.writeFBadWrongLock(), 2, UNSAFE_GUARDED_BY_ACCESS, [start of procedure writeFBadWrongLock()]
 codetoanalyze/java/infer/HashMapExample.java, int HashMapExample.getOneIntegerWithoutCheck(), 6, NULL_DEREFERENCE, [start of procedure getOneIntegerWithoutCheck()]
+codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getAfterClearBad(), 5, NULL_DEREFERENCE, [start of procedure getAfterClearBad()]
+codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getAfterRemovingTheKeyBad(), 5, NULL_DEREFERENCE, [start of procedure getAfterRemovingTheKeyBad()]
 codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getTwoIntegersWithOneCheck(Integer,Integer), 11, NULL_DEREFERENCE, [start of procedure getTwoIntegersWithOneCheck(...),Taking true branch,Taking true branch]
 codetoanalyze/java/infer/IntegerExample.java, void IntegerExample.testIntegerEqualsBad(), 6, NULL_DEREFERENCE, [start of procedure testIntegerEqualsBad(),Taking true branch]
 codetoanalyze/java/infer/InvokeDynamic.java, int InvokeDynamic.lambda$npeInLambdaBad$1(String,String), 1, NULL_DEREFERENCE, [start of procedure lambda$npeInLambdaBad$1(...)]

infer/tests/codetoanalyze/java/infer/HashMapExample.java

@@ -87,4 +87,28 @@ public class HashMapExample {
       x.toString();
   }
 
+  void getAfterRemovingTheKeyBad() {
+    HashMap<Integer, Object> map = new HashMap();
+    Integer key = 42;
+    map.put(key, new Object());
+    map.remove(key);
+    map.get(key).toString(); // NPE here
+  }
+
+  void getAfterRemovingAnotherKeyOk() {
+    HashMap<Integer, Object> map = new HashMap();
+    Integer key = 42;
+    map.put(key, new Object());
+    map.remove(0);
+    map.get(key).toString();
+  }
+
+  void getAfterClearBad() {
+    HashMap<Integer, Object> map = new HashMap();
+    Integer key = 42;
+    map.put(key, new Object());
+    map.clear();
+    map.get(key).toString(); // NPE here
+  }
+
 }

infer/tests/codetoanalyze/java/infer/issues.exp

@@ -98,6 +98,8 @@ codetoanalyze/java/infer/GuardedByExample.java, void GuardedByExample.writeFAfte
 codetoanalyze/java/infer/GuardedByExample.java, void GuardedByExample.writeFBad(), 1, UNSAFE_GUARDED_BY_ACCESS, [start of procedure writeFBad()]
 codetoanalyze/java/infer/GuardedByExample.java, void GuardedByExample.writeFBadWrongLock(), 2, UNSAFE_GUARDED_BY_ACCESS, [start of procedure writeFBadWrongLock()]
 codetoanalyze/java/infer/HashMapExample.java, int HashMapExample.getOneIntegerWithoutCheck(), 6, NULL_DEREFERENCE, [start of procedure getOneIntegerWithoutCheck()]
+codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getAfterClearBad(), 5, NULL_DEREFERENCE, [start of procedure getAfterClearBad()]
+codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getAfterRemovingTheKeyBad(), 5, NULL_DEREFERENCE, [start of procedure getAfterRemovingTheKeyBad()]
 codetoanalyze/java/infer/HashMapExample.java, void HashMapExample.getTwoIntegersWithOneCheck(Integer,Integer), 11, NULL_DEREFERENCE, [start of procedure getTwoIntegersWithOneCheck(...),Taking true branch,Taking true branch]
 codetoanalyze/java/infer/IntegerExample.java, void IntegerExample.testIntegerEqualsBad(), 6, NULL_DEREFERENCE, [start of procedure testIntegerEqualsBad(),Taking true branch]
 codetoanalyze/java/infer/InvokeDynamic.java, int InvokeDynamic.lambda$npeInLambdaBad$1(String,String), 1, NULL_DEREFERENCE, [start of procedure lambda$npeInLambdaBad$1(...)]