[Infer][models] Modeling Handler.postDelayed and similar to detect more Activity leaks

Summary: Handler.postDelayed keeps a persistent reference to its Runnable argument that may cause a memory leak if an Activity is reachable from the Runnable.

infer/models/java/src/android/os/Handler.java

@@ -0,0 +1,37 @@
+/*
+* 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 android.os;
+
+import com.facebook.infer.models.InferUndefined;
+
+class Handler {
+
+    // model queue of tasks using 1-recency abstraction
+    private static Runnable sFakeHandlerQueue;
+
+    public final boolean postDelayed(Runnable r, long delayMillis) {
+        // model posting a delayed message as keeping a persistent reference to the Runnable
+        sFakeHandlerQueue = r;
+        return InferUndefined.boolean_undefined();
+    }
+
+    public final void removeCallbacks(Runnable r) {
+        if (r == sFakeHandlerQueue)
+            sFakeHandlerQueue = null;
+    }
+
+    public final void removeCallbacks(Runnable r, Object token) {
+        removeCallbacks(r);
+    }
+
+    public final void removeCallbacksAndMessages(Object token) {
+        sFakeHandlerQueue = null;
+    }
+}

infer/src/backend/localise.ml

@@ -367,9 +367,12 @@ let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc =
 let desc_activity_leak pname activity_typ fieldname : error_desc =
   let pname_str = Procname.java_get_class pname ^ "." ^ Procname.java_get_method pname in
   (* intentionally omit space; [typ_to_string] adds an extra space *)
-  let activity_str = Sil.typ_to_string activity_typ ^ "may leak via static field" in
+  let activity_str = Sil.typ_to_string activity_typ ^ "may leak via" in
   let fld_str = Ident.fieldname_to_string fieldname in
-  (["Activity"; activity_str; fld_str; "during call to"; pname_str], None, [])
+  let leak_msg =
+    if fld_str = "android.os.Handler.sFakeHandlerQueue" then "call to Handler.postDelayed"
+    else "assignment to static field " ^ fld_str in
+  (["Activity"; activity_str; leak_msg; "during call to"; pname_str] , None, [])
 
 let desc_assertion_failure loc : error_desc =
   (["could be raised"; at_line (Tags.create ()) loc], None, [])

infer/tests/codetoanalyze/java/infer/ActivityLeaks.java

@@ -11,6 +11,7 @@ package codetoanalyze.java.infer;
 
 import android.app.Activity;
 import android.content.Context;
+import android.os.Handler;
 
 public class ActivityLeaks extends Activity {
 
@@ -89,4 +90,25 @@ public class ActivityLeaks extends Activity {
         return Singleton.getInstance(this.getApplicationContext());
     }
 
+    private Handler handler = new Handler();
+
+    public void handlerLeak() {
+        Runnable r =
+            new Runnable() {
+                public void run() {
+                }
+            };
+        handler.postDelayed(r, 10000);
+    }
+
+    public void handlerNoLeak() {
+        Runnable r =
+            new Runnable() {
+                public void run() {
+                }
+            };
+        handler.postDelayed(r, 10000);
+        handler.removeCallbacks(r);
+    }
+
 }

infer/tests/endtoend/java/infer/ActivityLeaksTest.java

@@ -44,7 +44,8 @@ public class ActivityLeaksTest {
         "indirectLeak",
         "nonStaticInnerClassLeak",
         "leakAfterInstanceFieldWrite",
-        "singletonLeak"
+        "singletonLeak",
+        "handlerLeak"
     };
     assertThat(
         "Results should contain " + ACTIVITY_LEAK,